ωCPO instance for coproducts

This file provides the OmegaCompletePartialOrder instance for Sum α β.

noncomputable instance OmegaCompletePartialOrder.Sum.instSum_quasiBorelSpaces {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : OmegaCompletePartialOrder (α ⊕ β)

Equations

• One or more equations did not get rendered due to their size.

theorem OmegaCompletePartialOrder.Sum.ωSup_def {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain (α ⊕ β)) : ωSup c = Sum.map ωSup ωSup (Chain.Sum.distrib c)

theorem OmegaCompletePartialOrder.Sum.lt_def {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (a✝ a✝¹ : α ⊕ β) : (a✝ < a✝¹) = Sum.LiftRel (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : β) => x1 < x2) a✝ a✝¹

theorem OmegaCompletePartialOrder.Sum.le_def {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (a✝ a✝¹ : α ⊕ β) : (a✝ ≤ a✝¹) = Sum.LiftRel (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) a✝ a✝¹

@[simp]

theorem OmegaCompletePartialOrder.Sum.ωSup_inl {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain α) : ωSup (Chain.Sum.inl c) = Sum.inl (ωSup c)

@[simp]

theorem OmegaCompletePartialOrder.Sum.ωSup_inr {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain β) : ωSup (Chain.Sum.inr c) = Sum.inr (ωSup c)

theorem OmegaCompletePartialOrder.Sum.ωSup_projl {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [Inhabited α] (c : Chain (α ⊕ β)) : ωSup (Chain.Sum.projl c) = Sum.elim id (fun (x : β) => default) (ωSup c)