cast_card — Mathlib

English

If α is finite, then (Nat.card α) as a Cardinal equals Cardinal.mk α.

Русский

Если множество α конечное, то (Nat.card α) как кардинал равен Cardinal.mk α.

LaTeX

$$$ [\mathrm{Finite}\,\alpha] \rightarrow (\mathrm{Nat.card}\alpha : \mathrm{Cardinal}) = \mathrm{Cardinal.mk}\alpha $$$

Lean4

theorem cast_card [Finite α] : (Nat.card α : Cardinal) = Cardinal.mk α :=
  by
  rw [Nat.card, Cardinal.cast_toNat_of_lt_aleph0]
  exact Cardinal.lt_aleph0_of_finite _

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