finite_subsets — Mathlib

English

There are finitely many subsets of a finite set a.

Русский

Существенно конечное число подмножеств конечного множества a.

LaTeX

$$$ \forall a : \mathrm{Set}\alpha, \mathrm{Finite}(a) \rightarrow \mathrm{Finite}(\{ b \mid b \subseteq a \})$$$

Lean4

/-- There are finitely many subsets of a given finite set -/
theorem finite_subsets {α : Type u} {a : Set α} (h : a.Finite) : {b | b ⊆ a}.Finite :=
  by
  convert ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet
  ext s
  simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset, ← and_assoc, Finset.coeEmb] using
    h.subset

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