top_notMem

Mathlib.Order.UpperLower.Basic

URI: https://scilib.ai/kg/mathlib#IsUpperSet.top_notMem

English

For an upper set, top does not belong to the set iff the set is empty.

Русский

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

LaTeX

$$top_notMem (hs : IsUpperSet s) : ⊤ ∉ s ↔ s = ∅$$

Lean4

theorem top_notMem (hs : IsUpperSet s) : ⊤ ∉ s ↔ s = ∅ :=
  hs.top_mem.not.trans not_nonempty_iff_eq_empty

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru