univ_eq_empty_iff — Mathlib

English

The univ and empty sets are equal if and only if the base type is empty.

Русский

Унивальная и пустая множества равны тогда и только тогда, когда базовый тип пуст.

LaTeX

$$$(\mathrm{univ} : \mathrm{Set} \alpha) = \emptyset \; \Leftrightarrow \mathrm{IsEmpty} \alpha$$$

Lean4

@[simp]
theorem univ_eq_empty_iff : (univ : Set α) = ∅ ↔ IsEmpty α :=
  eq_empty_iff_forall_notMem.trans ⟨fun H => ⟨fun x => H x trivial⟩, fun H x _ => @IsEmpty.false α H x⟩

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