mk_eq_nat_iff_finset — Mathlib

English

|α| = n iff there exists t : Finset α with (t:Set α) = univ and t.card = n.

Русский

Кардинал множества α равен n тогда и только тогда существует t : Finset α такое, что (t:Set α) = univ и t.card = n.

LaTeX

$$$|\\alpha| = n \\iff \\exists t : Finset \\alpha, (t : Set \\alpha) = \\mathrm{univ} \\land t.card = n$$$

Lean4

theorem mk_eq_nat_iff_finset {n : ℕ} : #α = n ↔ ∃ t : Finset α, (t : Set α) = univ ∧ t.card = n := by
  rw [← mk_univ, mk_set_eq_nat_iff_finset]

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