English
For any f, a, m with injOn on the preimage of the support of single (f a) m, comapDomain f (single (f a) m) hif = single a m.
Русский
Для любого f, a и m существует injOn на предпредокоме поддержки single (f a) m: comapDomain f (single (f a) m) hif = single a m.
LaTeX
$$$$ comapDomain\ f\ (\mathrm{single}(f a) m)\ hif = \mathrm{single}(a) m. $$$$
Lean4
@[simp]
theorem comapDomain_single (f : α → β) (a : α) (m : M) (hif : Set.InjOn f (f ⁻¹' (single (f a) m).support)) :
comapDomain f (Finsupp.single (f a) m) hif = Finsupp.single a m :=
by
rcases eq_or_ne m 0 with (rfl | hm)
· simp_rw [single_zero, comapDomain_zero]
· rw [eq_single_iff, comapDomain_apply, comapDomain_support, ← Finset.coe_subset, coe_preimage,
support_single_ne_zero _ hm, coe_singleton, coe_singleton, single_eq_same]
rw [support_single_ne_zero _ hm, coe_singleton] at hif
exact ⟨fun x hx => hif hx rfl hx, rfl⟩
