Theorems · Theorem · order theory

HahnEmbedding.ArchimedeanStrata.mk.injEq

∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (stratum : FiniteArchimedeanClass M → Submodule K M)
  (disjoint_ball_stratum : ∀ (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (stratum c))
  (ball_sup_stratum_eq :
    ∀ (c : FiniteArchimedeanClass M),
      FiniteArchimedeanClass.ball K c ⊔ stratum c = FiniteArchimedeanClass.closedBall K c)
  (stratum_1 : FiniteArchimedeanClass M → Submodule K M)
  (disjoint_ball_stratum_1 : ∀ (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (stratum_1 c))
  (ball_sup_stratum_eq_1 :
    ∀ (c : FiniteArchimedeanClass M),
      FiniteArchimedeanClass.ball K c ⊔ stratum_1 c = FiniteArchimedeanClass.closedBall K c),
  ({ stratum := stratum, disjoint_ball_stratum := disjoint_ball_stratum, ball_sup_stratum_eq := ball_sup_stratum_eq } =
      { stratum := stratum_1, disjoint_ball_stratum := disjoint_ball_stratum_1,
        ball_sup_stratum_eq := ball_sup_stratum_eq_1 }) =
    (stratum = stratum_1)

Defined in

Mathlib.Algebra.Order.Module.HahnEmbedding

Cited by

0 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingLinearOrderIsOrderedRingArchimedeanAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsOrderedModule