map_injective — Mathlib

English

If the underlying function f is injective, then the induced map on unitary subgroups is injective.

Русский

Если базовое отображение f инъективно, то порождаемое отображение между унитарными подгруппами также инъективно.

LaTeX

$$$hf:\\,\\text{Injective} \\implies \\mathrm{map} f \\text{ is injective}$$$

Lean4

@[simp]
theorem map_injective {f : R →⋆* S} (hf : Function.Injective f) : Function.Injective (map f : unitary R → unitary S) :=
  Subtype.map_injective (fun _ ↦ map_mem f) hf

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