English
The first isomorphism theorem for sets: the quotient of α by the kernel of a function f is bijective with the image of f.
Русский
Первая теорема о гомоморфизмах для множеств: фактор-множество α по ker f изоморфно образу функции f.
LaTeX
$$$$ \\ Quotient(\\ker f) \\ \\cong \\ Set.range f. $$$$
Lean4
/-- The first isomorphism theorem for sets: the quotient of α by the kernel of a function f
bijects with f's image. -/
noncomputable def quotientKerEquivRange : Quotient (ker f) ≃ Set.range f :=
Equiv.ofBijective
((@Quotient.lift _ (Set.range f) (ker f) fun x => ⟨f x, Set.mem_range_self x⟩) fun _ _ h => Subtype.ext h)
⟨fun x y h => ker_lift_injective f <| by rcases x with ⟨⟩; rcases y with ⟨⟩; injections, fun ⟨_, z, hz⟩ =>
⟨@Quotient.mk'' _ (ker f) z, Subtype.ext_iff.2 hz⟩⟩
