embDomain_inj — Mathlib

English

For l1, l2 ∈ α →₀ M, embDomain f l1 = embDomain f l2 if and only if l1 = l2, whenever f is an embedding α ↪ β. In particular embDomain f is injective.

Русский

Для l1, l2 ∈ α →₀ M верно embDomain f l1 = embDomain f l2 тогда и только тогда, когда l1 = l2, при условии, что f — вложение α ↪ β. В частности embDomain f инъективно.

LaTeX

$$$\\forall {α β : Type*} {M : Type*} [Zero M] (f : Function.Embedding α β) {l_1 l_2 : (α →_0 M)},\\ embDomain f l_1 = embDomain f l_2 \\iff l_1 = l_2$$$

Lean4

@[simp]
theorem embDomain_inj {f : α ↪ β} {l₁ l₂ : α →₀ M} : embDomain f l₁ = embDomain f l₂ ↔ l₁ = l₂ :=
  (embDomain_injective f).eq_iff

Похожие утверждения