univ_set_of_isEmpty — Mathlib

English

If α is empty, then the only subset of α is ∅; consequently, the universe of Set α is the singleton {∅}.

Русский

Если α пуст, единственным подмножеством α является пустое множество ∅; следовательно, множество Set α состоит из одного элемента — {∅}.

LaTeX

$$$ \mathrm{univ}_{\mathrm{Set}\,\alpha} = \{ \emptyset \}$$$

Lean4

@[simp]
theorem univ_set_of_isEmpty [IsEmpty α] : @univ (Set α) = {∅} :=
  subset_antisymm (fun S hS ↦ by simp [Set.eq_empty_of_isEmpty S]) (by simp)

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