ker_lift_injective — Mathlib

English

The map quotients ker f to β is injective: Quotient.lift f (ker f) is injective.

Русский

Отображение из фактор-множества по ядру f в β инъективно: Quotient.lift f (ker f) инъективно.

LaTeX

$$$$ Injective (Quotient.lift f (ker f) ). $$$$

Lean4

/-- Given a map f from α to β, the natural map from the quotient of α by the kernel of f is
injective. -/
theorem ker_lift_injective (f : α → β) : Injective (@Quotient.lift _ _ (ker f) f fun _ _ h => h) := fun x y =>
  Quotient.inductionOn₂' x y fun _ _ h => Quotient.sound' h

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