mk_set_eq_nat_iff_finset — Mathlib

English

For any set s and natural n, |s| = n if and only if there exists a Finset t with (t:Set α) = s and t.card = n.

Русский

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

LaTeX

$$$|s| = n \\iff \\exists t : Finset \\alpha, (t : Set \\alpha) = s \\land t.card = n$$$

Lean4

theorem mk_set_eq_nat_iff_finset {α} {s : Set α} {n : ℕ} : #s = n ↔ ∃ t : Finset α, (t : Set α) = s ∧ t.card = n :=
  by
  constructor
  · intro h
    lift s to Finset α using lt_aleph0_iff_set_finite.1 (h.symm ▸ nat_lt_aleph0 n)
    simpa using h
  · rintro ⟨t, rfl, rfl⟩
    exact mk_coe_finset

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