Archimedean classes for ordered module

Main definitions

• ArchimedeanClass.ball are ArchimedeanClass.ballAddSubgroup as a submodules.
• ArchimedeanClass.closedBall are ArchimedeanClass.closedBallAddSubgroup as a submodules.

@[simp]

theorem ArchimedeanClass.mk_smul {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {K : Type u_2} [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] (a : M) {k : K} (h : k ≠ 0) : mk (k • a) = mk a

theorem ArchimedeanClass.mk_le_mk_smul {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {K : Type u_2} [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] (a : M) (k : K) : mk a ≤ mk (k • a)

noncomputable def FiniteArchimedeanClass.submodule {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] (s : UpperSet (FiniteArchimedeanClass M)) : Submodule K M

Given an upper set s of finite archimedean classes in a linearly ordered module M with Archimedean scalars, all elements belonging to these classes together with 0 form a submodule.

This has the same carrier as FiniteArchimedeanClass.addSubgroup.

Equations

• FiniteArchimedeanClass.submodule K s = { toAddSubmonoid := (FiniteArchimedeanClass.addSubgroup s).toAddSubmonoid, smul_mem' := ⋯ }

theorem FiniteArchimedeanClass.submodule_strictAnti {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] : StrictAnti (submodule K)

@[reducible, inline]

noncomputable abbrev FiniteArchimedeanClass.ball {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] (c : FiniteArchimedeanClass M) : Submodule K M

An open ball defined by ArchimedeanClass.submodule of UpperSet.Ioi c. For c = ⊤, we assign the junk value ⊥.

This has the same carrier as ArchimedeanClass.ballAddSubgroup's.

Equations

• FiniteArchimedeanClass.ball K c = FiniteArchimedeanClass.submodule K (UpperSet.Ioi c)

@[reducible, inline]

noncomputable abbrev FiniteArchimedeanClass.closedBall {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] (c : FiniteArchimedeanClass M) : Submodule K M

A closed ball defined by ArchimedeanClass.submodule of UpperSet.Ici c.

This has the same carrier as ArchimedeanClass.closedBallAddSubgroup's.

Equations

• FiniteArchimedeanClass.closedBall K c = FiniteArchimedeanClass.submodule K (UpperSet.Ici c)

@[simp]

theorem FiniteArchimedeanClass.toAddSubgroup_ball {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] (c : FiniteArchimedeanClass M) : (ball K c).toAddSubgroup = c.ballAddSubgroup

@[simp]

theorem FiniteArchimedeanClass.toAddSubgroup_closedBall {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] (c : FiniteArchimedeanClass M) : (closedBall K c).toAddSubgroup = c.closedBallAddSubgroup

@[simp]

theorem FiniteArchimedeanClass.mem_ball_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] {a : M} {c : FiniteArchimedeanClass M} : a ∈ ball K c ↔ ∀ (h : a ≠ 0), c < mk a h

@[simp]

theorem FiniteArchimedeanClass.mem_closedBall_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] {a : M} {c : FiniteArchimedeanClass M} : a ∈ closedBall K c ↔ ∀ (h : a ≠ 0), c ≤ mk a h

theorem FiniteArchimedeanClass.ball_strictAnti {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] : StrictAnti (ball K)

theorem FiniteArchimedeanClass.ball_lt_closedBall {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (K : Type u_2) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [Module K M] [PosSMulMono K M] {c : FiniteArchimedeanClass M} : ball K c < closedBall K c