coe_nonempty — Mathlib

English

A closed set is nonempty if and only if its underlying set is nonempty, equivalently the top element is not bottom.

Русский

Замкнутое множество непусто тогда, когда его множество непусто; эквивалентно тому, что верхний элемент не равен нижнему.

LaTeX

$$$(s : \mathrm{Closeds}(\alpha)).\mathrm{Nonempty} \iff s \neq \bot.$$$

Lean4

theorem coe_nonempty {s : Closeds α} : (s : Set α).Nonempty ↔ s ≠ ⊥ :=
  nonempty_iff_ne_empty.trans coe_eq_empty.not

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