English
A refined lemma giving exact value of mapDomain on a a ∈ S assuming injectivity on S and support conditions.
Русский
Уточнённая лемма для точного значения mapDomain на a ∈ S при условии инъективности на S и опорных условиях.
LaTeX
$$$\\forall S\\; {f} \\;{x}\\; {hS}\\; {hf}\\; {a}\\; (ha) :\\; mapDomain f x (f a) = x a.$$$
Lean4
theorem mapDomain_apply' (S : Set α) {f : α → β} (x : α →₀ M) (hS : (x.support : Set α) ⊆ S) (hf : Set.InjOn f S)
{a : α} (ha : a ∈ S) : mapDomain f x (f a) = x a := by
classical
rw [mapDomain, sum_apply, sum]
simp_rw [single_apply]
by_cases hax : a ∈ x.support
· rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
convert add_zero (x a)
refine Finset.sum_eq_zero fun i hi => if_neg ?_
exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
· rw [notMem_support_iff.1 hax]
refine Finset.sum_eq_zero fun i hi => if_neg ?_
exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)
