Theorems · Theorem · order theory

HahnEmbedding.Partial.coeff_eq_of_mem

∀ {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] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] (x : M) {y z : ↥(↑f).domain} {c : FiniteArchimedeanClass M},
  ↑y - x ∈ FiniteArchimedeanClass.ball K c →
    ↑z - x ∈ FiniteArchimedeanClass.ball K c →
      ∀ {d : FiniteArchimedeanClass M}, d ≤ c → (ofLex (↑↑f y)).coeff d = (ofLex (↑↑f z)).coeff d

When y and z are both near x (the difference is in a ball), initial coefficients of f.val y and f.val z agree.

Defined in

Mathlib.Algebra.Order.Module.HahnEmbedding

Cited by

2 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderIsOrderedRingArchimedeanAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsOrderedModuleAddCommGroupLinearOrderModuleIsOrderedAddMonoidArchimedean