card — Mathlib

English

Nat.card α is the cardinality of α as a natural number; if α is infinite, Nat.card α = 0.

Русский

Nat.card α есть кардинальность α как натуральное число; если α бесконечно, Nat.card α = 0.

LaTeX

$$Nat.card(\\alpha) = toNat(|\\alpha|) \n\\land (Infinite(\\alpha) \\Rightarrow Nat.card(\\alpha) = 0)$$

Lean4

/-- `Nat.card α` is the cardinality of `α` as a natural number.
  If `α` is infinite, `Nat.card α = 0`. -/
protected def card (α : Type*) : ℕ :=
  toNat (mk α)

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