mk_eq_nat_iff_fintype — Mathlib

English

|α| = n iff there exists h : Fintype α with Fintype.card α h = n.

Русский

Кардинал множества α равен n тогда и только тогда существует структуру Fintype на α, для которой card α равна n.

LaTeX

$$$|\\alpha| = n \\iff \\exists h : Fintype \\alpha, @Fintype.card \\alpha h = n$$$

Lean4

theorem mk_eq_nat_iff_fintype {n : ℕ} : #α = n ↔ ∃ h : Fintype α, @Fintype.card α h = n :=
  by
  rw [mk_eq_nat_iff_finset]
  constructor
  · rintro ⟨t, ht, hn⟩
    exact ⟨⟨t, eq_univ_iff_forall.1 ht⟩, hn⟩
  · rintro ⟨⟨t, ht⟩, hn⟩
    exact ⟨t, eq_univ_iff_forall.2 ht, hn⟩

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