Theorems · Theorem · order theory

HahnEmbedding.Partial.eval_eq_truncLT

∀ {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)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} {c : FiniteArchimedeanClass M} {y : ↥(↑f).domain},
  ArchimedeanClass.mk (↑y - x) = ↑c →
    (∀ (z : ↥(↑f).domain), ↑z - x ∉ FiniteArchimedeanClass.ball K c) →
      f.eval x = toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑↑f y)))

If there is a y in f's domain with c = ArchimedeanClass (y - x), but there is no closer z to x where the difference is of a higher ArchimedeanClass, then f.eval x is simply f.val y truncated at c. This doesn't mean every x can be evaluated this way: it is possible that one can find an infinite chain of y that keeps getting closer to x in terms of Archimedean classes, yet x is still isolated within a very high Archimedean class. In fact, in the next theorem, we will show that there is always such chain for x not in f's domain.

Defined in

Mathlib.Algebra.Order.Module.HahnEmbedding

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderIsOrderedRingArchimedeanAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsOrderedModuleAddCommGroupLinearOrderModuleIsOrderedAddMonoidArchimedean