English
For any directed nonempty c, sSupFun hc is a partial embedding.
Русский
Для любого направленного непустого множества c, sSupFun hc — частичное вложение.
LaTeX
$$$\\text{IsPartial}(sSupFun hc)$$$
Lean4
theorem truncLT_mem_range_sSupFun {c : Set (Partial seed)} (hnonempty : c.Nonempty) (hc : DirectedOn (· ≤ ·) c)
(x : (sSupFun hc).domain) (c : FiniteArchimedeanClass M) :
toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (sSupFun hc x))) ∈ LinearMap.range (sSupFun hc).toFun :=
by
obtain hx := x.prop
simp_rw [sSupFun, LinearPMap.domain_sSup] at hx
obtain ⟨f, hmem, hf⟩ := (LinearPMap.mem_domain_sSup_iff (hnonempty.image _) (hc.mono_comp (by simp))).mp hx
obtain ⟨f', hmem', hf'⟩ := (Set.mem_image _ _ _).mp hmem
obtain h := (hf'.symm ▸ f'.prop.truncLT_mem_range) ⟨x, hf⟩ c
simp_rw [LinearMap.mem_range, LinearPMap.toFun_eq_coe] at ⊢ h
obtain ⟨x', hx'⟩ := h
have hmem' : x'.val ∈ (sSupFun hc).domain :=
by
apply Set.mem_of_mem_of_subset x'.prop
exact hf'.symm ▸ (le_sSupFun hc hmem').1
refine ⟨⟨x'.val, hmem'⟩, ?_⟩
have hleft : sSupFun hc ⟨x'.val, hmem'⟩ = f x' := LinearPMap.sSup_apply _ hmem _
have hright : sSupFun hc x = f ⟨x, hf⟩ := LinearPMap.sSup_apply _ hmem ⟨x, hf⟩
simpa [hleft, hright] using hx'
