English
If f is injective, then comapDomain f (v1 + v2) hf.injOn = comapDomain f v1 hf.injOn + comapDomain f v2 hf.injOn.
Русский
Если f инъективен, то comapDomain f (v1 + v2) hf.injOn = comapDomain f v1 hf.injOn + comapDomain f v2 hf.injOn.
LaTeX
$$$$ \mathrm{comapDomain}\ f\ (v_1 + v_2)\ hf.injOn = \mathrm{comapDomain}\ f\ v_1\ hf.injOn + \mathrm{comapDomain}\ f\ v_2\ hf.injOn. $$$$
Lean4
/-- Given `f : α → β`, `l : β →₀ M` and a proof `hf` that `f` is injective on
the preimage of `l.support`, `comapDomain f l hf` is the finitely supported function
from `α` to `M` given by composing `l` with `f`. -/
@[simps support]
def comapDomain [Zero M] (f : α → β) (l : β →₀ M) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : α →₀ M
where
support := l.support.preimage f hf
toFun a := l (f a)
mem_support_toFun := by
intro a
rw [Finset.mem_preimage]
exact l.mem_support_toFun (f a)
