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 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]

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]

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]

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]

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]

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]

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]

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]

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 ⊤ = ⊥

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)