powerset_eq_univ

Mathlib.Data.Fintype.Powerset

URI: https://scilib.ai/kg/mathlib#Finset.powerset_eq_univ

English

For a finite α, s.powerset = univ iff s = univ.

Русский

Для конечного α, если powerset(s) = univ, то s = univ, и наоборот.

LaTeX

$$$s.powerset = univ \\;\\iff\\; s = univ$$$

Lean4

@[simp]
theorem powerset_eq_univ : s.powerset = univ ↔ s = univ := by rw [← Finset.powerset_univ, powerset_inj]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru