powersetCard_self — Mathlib

English

The set of all subsets of s of size card(s) is the singleton {s}.

Русский

Множество всех подмножеств s размерности card(s) есть единственный элемент {s}.

LaTeX

$$powersetCard s.card s = { s }$$

Lean4

@[simp]
theorem powersetCard_self (s : Finset α) : powersetCard s.card s = { s } :=
  by
  ext
  rw [mem_powersetCard, mem_singleton]
  constructor
  · exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge
  · rintro rfl
    simp

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