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)

@[deprecated FiniteArchimedeanClass.submodule (since := "2025-12-14")]

noncomputable def ArchimedeanClass.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 (ArchimedeanClass M)) : Submodule K M

Given an upper set s of archimedean classes in a linearly ordered module M with Archimedean scalars, all elements belonging to these classes form a submodule, except when s = ⊤ for which the set would be empty. For s = ⊤, we assign the junk value ⊥.

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

Equations

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

@[reducible, inline, deprecated FiniteArchimedeanClass.ball (since := "2025-12-14")]

noncomputable abbrev ArchimedeanClass.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 : ArchimedeanClass 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

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

@[reducible, inline, deprecated FiniteArchimedeanClass.closedBall (since := "2025-12-14")]

noncomputable abbrev ArchimedeanClass.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 : ArchimedeanClass 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

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

@[simp, deprecated FiniteArchimedeanClass.toAddSubgroup_ball (since := "2025-12-14")]

theorem ArchimedeanClass.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 : ArchimedeanClass M) : (ball K c).toAddSubgroup = c.ballAddSubgroup

@[simp, deprecated FiniteArchimedeanClass.toAddSubgroup_closedBall (since := "2025-12-14")]

theorem ArchimedeanClass.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 : ArchimedeanClass M) : (closedBall K c).toAddSubgroup = c.closedBallAddSubgroup

@[simp, deprecated FiniteArchimedeanClass.mem_ball_iff (since := "2025-12-14")]

theorem ArchimedeanClass.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 : ArchimedeanClass M} (hc : c ≠ ⊤) : a ∈ ball K c ↔ c < mk a

@[simp, deprecated FiniteArchimedeanClass.mem_closedBall_iff (since := "2025-12-14")]

theorem ArchimedeanClass.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 : ArchimedeanClass M} : a ∈ closedBall K c ↔ c ≤ mk a

@[simp, deprecated "Lemma for junk value." (since := "2025-12-14")]

theorem ArchimedeanClass.ball_top (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] : ball K ⊤ = ⊥

@[simp, deprecated "Lemma for junk value." (since := "2025-12-14")]

theorem ArchimedeanClass.closedBall_top (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] : closedBall K ⊤ = ⊥

@[deprecated FiniteArchimedeanClass.ball_strictAnti (since := "2025-12-14")]

theorem ArchimedeanClass.ball_antitone {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] : Antitone (ball K)

@[deprecated FiniteArchimedeanClass.ball_lt_closedBall (since := "2025-12-14")]

theorem ArchimedeanClass.ball_le_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 : ArchimedeanClass M} : ball K c ≤ closedBall K c

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