ncard_le_card — Mathlib

English

If α is finite, then for any subset s of α, the ncard of s does not exceed the cardinality of α.

Русский

Если α конечен, то для любого подмножества s ⊆ α кардинал mножества s не превосходит кардинал α.

LaTeX

$$$ [\#\alpha < \infty] \Rightarrow |s| \le |\alpha| $$$

Lean4

theorem ncard_le_card [Finite α] (s : Set α) : s.ncard ≤ Nat.card α :=
  ncard_univ α ▸ ncard_le_ncard s.subset_univ

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