univ_set_eq_singleton_empty_iff — Mathlib

English

The universal set of Set α equals {∅} if and only if α is empty.

Русский

Универсум множества Set α равен {∅} тогда и только тогда, когда α пуст.

LaTeX

$$$ \mathrm{univ} = \{ \emptyset \} \iff \mathrm{IsEmpty}(\alpha)$$$

Lean4

@[simp]
theorem univ_set_eq_singleton_empty_iff : @Set.univ (Set α) = {∅} ↔ IsEmpty α :=
  by
  refine ⟨fun h ↦ ?_, fun _ ↦ by simp⟩
  suffices @univ α ∈ univ by aesop
  simp

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