ncard_lt_card — Mathlib

English

Let α be a finite type. If s is a proper subset of α (i.e., s ≠ α), then the finite cardinality of s is strictly smaller than the cardinality of α.

Русский

Пусть α конечного типа. Если s является правильным подмножеством α (то есть s ≠ α), то конечная кардинальность s строго меньше кардинальности α.

LaTeX

$$$$ [\mathrm{Finite}(\alpha)] \Rightarrow \forall s \subseteq \alpha,\ s \neq \alpha \Rightarrow |s| < |\alpha| $$$$

Lean4

theorem ncard_lt_card [Finite α] (h : s ≠ univ) : s.ncard < Nat.card α :=
  ncard_univ α ▸ ncard_lt_ncard (ssubset_univ_iff.mpr h)

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