sized_powersetCard — Mathlib

English

Every element of powersetCard r s has size r; i.e., the r-subsets of s all have cardinality r.

Русский

Каждый элемент powersetCard r s имеет размер r; то есть все r-подмножества s имеют кардинал r.

LaTeX

$$$\\forall t\\,(t \\in\\ powersetCard(r,s)\\Rightarrow |t| = r).$$$

Lean4

theorem sized_powersetCard (s : Finset α) (r : ℕ) : (powersetCard r s : Set (Finset α)).Sized r := fun _t ht =>
  (mem_powersetCard.1 ht).2

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