Documentation

Mathlib.Algebra.Order.Module.Archimedean

Archimedean classes for ordered module #

Main definitions #

source
@[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
source
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)
source
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
Instances For
    source
    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)
    source
    @[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
    Instances For
      source
      @[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
      Instances For
        source
        @[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
        source
        @[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
        source
        @[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
        source
        @[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
        source
        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)
        source
        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