ωSup_eq_none

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#Part.ωSup_eq_none

English

Another variant: if there are no elements, ωSup equals none.

Русский

Ещё одна версия: если нет элементов, ωSup равно none.

LaTeX

$$$$ \text{If } \neg \exists a, \text{some } a \in c, \ Part.ωSup c = none. $$$$

Lean4

theorem ωSup_eq_none {c : Chain (Part α)} (h : ¬∃ a, some a ∈ c) : Part.ωSup c = none :=
  dif_neg h

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

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

Разделы

Аффилиация

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