mapDomain_injective — Mathlib

English

If f is injective, then mapDomain f is injective as a function from α →₀ M to β →₀ M.

Русский

Если f инъективен, то mapDomain f инъективен как отображение из α →₀ M в β →₀ M.

LaTeX

$$$$ \mathrm{Function.Injective}(\mathrm{mapDomain}\ f). $$$$

Lean4

theorem mapDomain_injective {f : α → β} (hf : Function.Injective f) :
    Function.Injective (mapDomain f : (α →₀ M) → β →₀ M) :=
  by
  intro v₁ v₂ eq
  ext a
  have : mapDomain f v₁ (f a) = mapDomain f v₂ (f a) := by rw [eq]
  rwa [mapDomain_apply hf, mapDomain_apply hf] at this

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