eq_univ_iff_ncard — Mathlib

English

For finite α and any subset s ⊆ α, s = univ if and only if ncard s equals Nat.card α.

Русский

Для конечного α и любого подмножества s ⊆ α, s = univ тогда и только тогда, когда ncard s равно Nat.card α.

LaTeX

$$$$ s = \mathrm{univ} \iff s.ncard = \mathrm{Nat.card}(\alpha) $$$$

Lean4

theorem eq_univ_iff_ncard [Finite α] (s : Set α) : s = univ ↔ ncard s = Nat.card α := by
  rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, left_eq_add]

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