set_fintype_card_eq_univ_iff — Mathlib

English

Let α be finite and s ⊆ α with s finite. Then the cardinality of s equals the cardinality of α if and only if s is the whole universe, i.e. s = Set.univ.

Русский

Пусть α конечен и s ⊆ α, причём s конечно. Тогда кардинальность s равна кардинальности α тогда и только тогда, когда s есть всё множество, то есть s = Set.univ.

LaTeX

$$$|s| = |\alpha| \iff s = \mathrm{Set.univ}$$$

Lean4

theorem set_fintype_card_eq_univ_iff [Fintype α] (s : Set α) [Fintype s] :
    Fintype.card s = Fintype.card α ↔ s = Set.univ := by
  rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]

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