English
If f : α → β and hf : InjOn f S, then mapDomain f is injective on the set {w | w.support ⊆ S}.
Русский
Пусть f : α → β и hf : InjOn f S; тогда mapDomain f инъективно на множестве { w | w.support ⊆ S }.
LaTeX
$$$$ \mathrm{InjOn}(\mathrm{mapDomain}\ f, \{ w \mid w.\mathrm{support} \subseteq S \}). $$$$
Lean4
theorem mapDomain_injOn (S : Set α) {f : α → β} (hf : Set.InjOn f S) :
Set.InjOn (mapDomain f : (α →₀ M) → β →₀ M) {w | (w.support : Set α) ⊆ S} :=
by
intro v₁ hv₁ v₂ hv₂ eq
ext a
classical
by_cases h : a ∈ v₁.support ∪ v₂.support
·
rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq] <;>
· apply Set.union_subset hv₁ hv₂
exact mod_cast h
· simp_all
