univ_eq_empty_iff — Mathlib

English

The univ finset equals the singleton {∅} iff α is empty.

Русский

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

LaTeX

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

Lean4

theorem univ_eq_empty_iff : (univ : Finset α) = ∅ ↔ IsEmpty α := by
  rw [← not_nonempty_iff, ← univ_nonempty_iff, not_nonempty_iff_eq_empty]

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