finite_classes_ker — Mathlib

English

If β is finite, then the collection of equivalence classes of ker f is finite.

Русский

Если β конечна, то множество классов эквивалентности Ker(f) конечно.

LaTeX

$$$\\text{Finite}(\\beta) \\Rightarrow (\\ker f).\\mathrm{classes} \\\\text{Finite}.$$$

Lean4

theorem finite_classes_ker {α β : Type*} [Finite β] (f : α → β) : (Setoid.ker f).classes.Finite :=
  (Set.finite_range _).subset <| classes_ker_subset_fiber_set f

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