univ_nonempty_iff — Mathlib

English

For a finite type α, (univ : Finset α) is nonempty iff α is nonempty.

Русский

Для конечного типа α множество univ непусто тогда и только тогда, когда α непуст.

LaTeX

$$$ (univ : \\\\mathrm{Finset} \\\\alpha).\\\\Nonempty \\\\iff \\\\mathrm{Nonempty} \\\\alpha $$$

Lean4

theorem univ_nonempty_iff : (univ : Finset α).Nonempty ↔ Nonempty α := by
  rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]

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