English
The orderTop of the Lex encoding corresponds to a finite Archimedean class mk of x.
Русский
OrderTop лексикографического кодирования соответствует конечному Архимедовому классу mk x.
LaTeX
$$$ (\text{orderTop}) = (\text{FiniteArchimedeanClass.mk } x) $$$
Lean4
/-- Archimedean class of the input is transferred to `HahnSeries.orderTop`. -/
theorem orderTop_eq_archimedeanClassMk [IsOrderedAddMonoid R] [Archimedean R] (x : f.val.domain) :
FiniteArchimedeanClass.withTopOrderIso M (ofLex (f.val x)).orderTop = mk x.val :=
by
by_cases hx0 : x = 0
· simp [hx0]
have hx0' : x.val ≠ 0 := by simpa using hx0
have : Nontrivial (seed.stratum (mk x)) := by
apply seed.nontrivial_stratum
simpa using hx0
obtain ⟨⟨x', hx'mem⟩, hx'0⟩ := exists_ne (0 : seed.stratum (mk x))
have heq : mk x' = mk x.val := by
apply seed.archimedeanClassMk_of_mem_stratum hx'mem
simpa using hx'0
let x'' : f.val.domain := ⟨x', mem_domain f hx'mem⟩
have hx''mem : x''.val ∈ seed.stratum (FiniteArchimedeanClass.mk x.val hx0').val := hx'mem
have h0 : (seed.coeff (FiniteArchimedeanClass.mk x.val hx0').val) ⟨x''.val, hx''mem⟩ ≠ 0 :=
by
rw [(LinearMap.map_eq_zero_iff _ (seed.strictMono_coeff _).injective).ne]
unfold x''
simpa using hx'0
have heq' : mk x''.val = mk x.val := heq
rw [← orderTop_eq_iff, apply_of_mem_stratum f hx''mem, ofLex_toLex, HahnSeries.orderTop_single h0] at heq'
simp [← heq']
