univ_ofIsEmpty — Mathlib

English

If α is empty, then the univ under Fintype.ofIsEmpty equals ∅.

Русский

Если α пуст, то univ по Fintype.ofIsEmpty равен пустому множеству.

LaTeX

$$theorem univ_ofIsEmpty [IsEmpty α] : @univ α Fintype.ofIsEmpty = ∅$$

Lean4

/-- Note: this lemma is specifically about `Fintype.ofIsEmpty`. For a statement about
arbitrary `Fintype` instances, use `Finset.univ_eq_empty`. -/
theorem univ_ofIsEmpty [IsEmpty α] : @univ α Fintype.ofIsEmpty = ∅ :=
  rfl

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