omegaCompletePartialOrder

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#Part.omegaCompletePartialOrder

Lean4

noncomputable instance omegaCompletePartialOrder : OmegaCompletePartialOrder (Part α)
    where
  ωSup := Part.ωSup
  le_ωSup c
    i := by
    intro x hx
    rw [← eq_some_iff] at hx ⊢
    rw [ωSup_eq_some]
    rw [← hx]
    exact ⟨i, rfl⟩
  ωSup_le := by
    rintro c x hx a ha
    replace ha := mem_chain_of_mem_ωSup ha
    obtain ⟨i, ha⟩ := ha
    apply hx i
    rw [← ha]
    apply mem_some

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

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

Разделы

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

Аффилиация

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