Theorems · Theorem · order theory

HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq

∀ {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] (self : HahnEmbedding.ArchimedeanStrata K M)
  (c : FiniteArchimedeanClass M),
  FiniteArchimedeanClass.ball K c ⊔ self.stratum c = FiniteArchimedeanClass.closedBall K c

stratum and FiniteArchimedeanClass.ball are codisjoint under FiniteArchimedeanClass.closedBall.

Defined in

Mathlib.Algebra.Order.Module.HahnEmbedding

Cited by

3 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderIsOrderedRingArchimedeanAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsOrderedModule