instOmegaCompletePartialOrder

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#CompleteLattice.instOmegaCompletePartialOrder

Lean4

/-- Any complete lattice has an `ω`-CPO structure where the countable supremum is a special case
of arbitrary suprema. -/
instance (priority := 100) [CompleteLattice α] : OmegaCompletePartialOrder α
    where
  ωSup c := ⨆ i, c i
  ωSup_le := fun ⟨c, _⟩ s hs => by simpa only [iSup_le_iff]
  le_ωSup := fun ⟨c, _⟩ i => le_iSup_of_le i le_rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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