English
If f is injOn on s.support, then the support of mapDomain f s equals the image of s.support.
Русский
Если f инъективна на опоре s, то опора mapDomain f s равна образу опоры s.
LaTeX
$$$\\text{mapDomain}_f s).\\text{support} = \\mathrm{image} \\; s.\\text{support}$ under the given conditions.$$
Lean4
theorem mapDomain_support_of_injOn [DecidableEq β] {f : α → β} (s : α →₀ M) (hf : Set.InjOn f s.support) :
(mapDomain f s).support = Finset.image f s.support :=
Finset.Subset.antisymm mapDomain_support <| by
intro x hx
simp only [mem_image, mem_support_iff, Ne] at hx
rcases hx with ⟨hx_w, hx_h_left, rfl⟩
simp only [mem_support_iff, Ne]
rw [mapDomain_apply' (↑s.support : Set _) _ _ hf]
· exact hx_h_left
· simp_rw [mem_coe, mem_support_iff, Ne]
exact hx_h_left
· exact Subset.refl _
