isωSup_ωSup

Mathlib.Topology.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#isωSup_ωSup

English

For any chain c, IsωSup c (ωSup c) holds; i.e., ωSup is the ω-sup of c.

Русский

Для любой цепи c выполняется IsωSup c (ωSup c); ωSup есть ω-предел цепи.

LaTeX

$$IsωSup(c, ωSup(c)).$$

Lean4

theorem isωSup_ωSup {α} [OmegaCompletePartialOrder α] (c : Chain α) : IsωSup c (ωSup c) :=
  by
  constructor
  · apply le_ωSup
  · apply ωSup_le

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

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

Разделы

Аффилиация

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