mapOfSurjective_eq_map — Mathlib

English

Under surjectivity, the map defined by r equals the map defined by the surjective kernel map.

Русский

При сюръективности отображение, заданное отношением r, совпадает с отображением, заданным отображением по ker f через surjective.

LaTeX

$$$$ map\\ r\\ f = mapOfSurjective r f h hf. $$$$

Lean4

/-- A special case of the equivalence closure of an equivalence relation r equaling r. -/
theorem mapOfSurjective_eq_map (h : ker f ≤ r) (hf : Surjective f) : map r f = mapOfSurjective r f h hf := by
  rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]; rfl

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