English
If there is y in f’s domain whose Archimedean class equals c and there is no closer z to x with a higher class, then f.eval x equals the Lex-truncation of f.val y at c.
Русский
Если существует y в области определения f с mk(y − x) = c и нет близкого z к x с более высоким классом, то f.eval x равно Lex-трuncate для f.val y на c.
LaTeX
$$$f.eval x = \\mathrm{toLex}(\\ HahnSeries.truncLTLinearMap\\ K\\ c\\ (ofLex(f.val y)))$ при гипотезах hy и h.$$
Lean4
theorem extendFun_strictMono [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain) :
StrictMono (f.extendFun hx) :=
by
have hx' {c : K} (hc : c ≠ 0) : -c • x ∉ f.val.domain :=
by
contrapose! hx
rwa [neg_smul, neg_mem_iff, Submodule.smul_mem_iff _ hc] at hx
intro y z hyz
rw [← sub_pos] at hyz
apply lt_of_sub_pos
rw [← LinearPMap.map_sub]
obtain hyzmem := (z - y).prop
nth_rw 1 [extendFun, LinearPMap.domain_supSpanSingleton] at hyzmem
obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hyzmem
have : z - y = ⟨a + b, hab.symm ▸ (z - y).prop⟩ := by simp_rw [hab]
rw [this] at ⊢ hyz
have habpos : 0 < a + b := by exact hyz
obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hb
rw [← hc] at habpos
simp_rw [← hc, extendFun]
rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ hx _ ha]
suffices f.eval (-c • x) < f.val ⟨a, ha⟩ by
rw [eval_smul, neg_smul] at this
exact neg_lt_iff_pos_add.mp this
have hac : -c • x < a := by
rw [neg_smul]
exact neg_lt_iff_pos_add.mpr habpos
by_cases hc : c = 0
· rw [hc] at ⊢ hac
suffices f.val 0 < f.val ⟨a, ha⟩ by simpa using this
exact f.prop.strictMono (by simpa using hac)
· exact f.eval_lt (hx' hc) ⟨a, ha⟩ hac
