English
Let α, β be types and M a type with a zero element. If f is an embedding α ↪ β, then the corresponding extension-by-zero map embDomain f : (α →₀ M) → (β →₀ M) is injective; i.e., for all l1, l2 ∈ α →₀ M, embDomain f l1 = embDomain f l2 implies l1 = l2.
Русский
Пусть α, β — множества и M — множество с нулём. Если f — вложение α ↪ β, то отображение embDomain f : (α →₀ M) → (β →₀ M) инъективно; т.е. для любых l1, l2 ∈ α →₀ M верно embDomain f l1 = embDomain f l2 => l1 = l2.
LaTeX
$$$\\forall (α β : Type*) (M : Type*) [Zero M] (f : Function.Embedding α β), Injective (embDomain f : (α \\to_0 M) \\to (β \\to_0 M))$$$
Lean4
theorem embDomain_injective (f : α ↪ β) : Function.Injective (embDomain f : (α →₀ M) → β →₀ M) := fun l₁ l₂ h =>
ext fun a => by simpa only [embDomain_apply] using DFunLike.ext_iff.1 h (f a)
