English
The map sending p to p under lmapDomain has a straightforward description of its image.
Русский
Образ отображения, заданного через lmapDomain, описывается ясно через опорные множества.
LaTeX
$$$\mathrm{lmapDomain\_supported}(M,R,s) : \mathrm{supported}(M,R,s) \to \mathrm{Set}$$$
Lean4
theorem lmapDomain_supported (f : α → α') (s : Set α) :
(supported M R s).map (lmapDomain M R f) = supported M R (f '' s) := by
classical
cases isEmpty_or_nonempty α
· simp [s.eq_empty_of_isEmpty]
refine
le_antisymm
(map_le_iff_le_comap.2 <|
le_trans (supported_mono <| Set.subset_preimage_image _ _) (supported_comap_lmapDomain M R _ _))
?_
intro l hl
refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
· rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
exact Function.invFunOn_mem (by simpa using hl hc)
· rw [← LinearMap.comp_apply, ← lmapDomain_comp]
refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
exact Function.invFunOn_eq (by simpa using hl hc)
