card_classes_ker_le — Mathlib

English

If β is finite, then the number of equivalence classes of ker f does not exceed the number of elements of β: | (ker f).classes | ≤ |β|.

Русский

Если β конечна, то число классов Ker(f) не превосходит число элементов β: |(ker f).classes| ≤ |β|.

LaTeX

$$$| (\\ker f).\\mathrm{classes} | \\le |\\beta|.$$$

Lean4

theorem card_classes_ker_le {α β : Type*} [Fintype β] (f : α → β) [Fintype (Setoid.ker f).classes] :
    Fintype.card (Setoid.ker f).classes ≤ Fintype.card β := by
  classical exact le_trans (Set.card_le_card (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)

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