instOmegaCompletePartialOrder — Mathlib

English

There is an ωCPO structure on the product α × β, with ωSup defined by ωSupImpl, and componentwise ωSup_le and le_ωSup.

Русский

Существует структура ωCPO на произведении α × β, где ωSup задан как ωSupImpl, а свойства ωSup_le и le_ωSup рассматриваются по компонентам.

LaTeX

$$$\text{ωCPO}(\alpha \times \beta) \;\text{with} \; ωSup := Prod.ωSupImpl$$$

Lean4

@[simps! ωSup_fst ωSup_snd]
instance : OmegaCompletePartialOrder (α × β) where
  ωSup := Prod.ωSupImpl
  ωSup_le := fun _ _ h => ⟨ωSup_le _ _ fun i => (h i).1, ωSup_le _ _ fun i => (h i).2⟩
  le_ωSup c i := ⟨le_ωSup (c.map OrderHom.fst) i, le_ωSup (c.map OrderHom.snd) i⟩

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