powerset_eq_singleton_empty — Mathlib

English

Let S be a (finite) set. The power set of S is the singleton {∅} if and only if S is empty.

Русский

Пусть S — конечное множество. Множество подмножеств S равняется единственному элементу {∅} тогда и только тогда, когда S пусто.

LaTeX

$$$\mathcal{P}(s) = \{ \emptyset \} \iff s = \emptyset$$$

Lean4

@[simp]
theorem powerset_eq_singleton_empty : s.powerset = {∅} ↔ s = ∅ := by rw [← powerset_empty, powerset_inj]

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