mk_powerset — Mathlib

English

For any set s, the cardinality of its powerset is 2^{|s|}.

Русский

Для любого множества s кардинал его множества подмножеств равен 2^{|s|}.

LaTeX

$$$|\mathcal{P}(s)| = 2^{|s|}$$$

Lean4

/-- A variant of `Cardinal.mk_set` expressed in terms of a `Set` instead of a `Type`. -/
@[simp]
theorem mk_powerset {α : Type u} (s : Set α) : #(↥(𝒫 s)) = 2 ^ #(↥s) :=
  (mk_congr (Equiv.Set.powerset s)).trans mk_set

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