Chain utilities for coproducts of ωCPOs

This file provides utilities for working with chains in sum types, which are used to construct the ωCPO instance for coproducts.

def OmegaCompletePartialOrder.Chain.Sum.inl {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain A) : Chain (A ⊕ B)

Left injection for chains of sums.

Equations

• OmegaCompletePartialOrder.Chain.Sum.inl c = c.map { toFun := Sum.inl, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sum.inl_apply {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain A) (n : ℕ) : (inl c) n = _root_.Sum.inl (c n)

def OmegaCompletePartialOrder.Chain.Sum.inr {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain B) : Chain (A ⊕ B)

Right injection for chains of sums.

Equations

• OmegaCompletePartialOrder.Chain.Sum.inr c = c.map { toFun := Sum.inr, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sum.inr_apply {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain B) (n : ℕ) : (inr c) n = _root_.Sum.inr (c n)

def OmegaCompletePartialOrder.Chain.Sum.projl {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [Inhabited A] (c : Chain (A ⊕ B)) : Chain A

Projects left values out of a chain.

Equations

• OmegaCompletePartialOrder.Chain.Sum.projl c = { toFun := fun (n : ℕ) => Sum.elim id (fun (x : B) => default) (c n), monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sum.projl_coe {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [Inhabited A] (c : Chain (A ⊕ B)) (n : ℕ) : (projl c) n = Sum.elim id (fun (x : B) => default) (c n)

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sum.projl_apply {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [Inhabited A] (c : Chain (A ⊕ B)) (n : ℕ) : (projl c) n = Sum.elim id (fun (x : B) => default) (c n)

def OmegaCompletePartialOrder.Chain.Sum.projr {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [Inhabited B] (c : Chain (A ⊕ B)) : Chain B

Projects right values out of a chain.

Equations

• OmegaCompletePartialOrder.Chain.Sum.projr c = OmegaCompletePartialOrder.Chain.Sum.projl (c.map { toFun := Sum.swap, monotone' := ⋯ })

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sum.projr_apply {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [Inhabited B] (c : Chain (A ⊕ B)) (n : ℕ) : (projr c) n = Sum.elim (fun (x : A) => default) id (c n)

def OmegaCompletePartialOrder.Chain.Sum.distrib {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain (A ⊕ B)) : Chain A ⊕ Chain B

Splits a chain of sums into a sum of chains.

Equations

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

theorem OmegaCompletePartialOrder.Chain.Sum.distrib_def {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [Inhabited A] [Inhabited B] (c : Chain (A ⊕ B)) : distrib c = if (c 0).isLeft = true then _root_.Sum.inl (projl c) else _root_.Sum.inr (projr c)

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sum.elim_distrib {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain (A ⊕ B)) : Sum.elim inl inr (distrib c) = c

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sum.distrib_inl {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain A) : distrib (inl c) = _root_.Sum.inl c

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sum.distrib_inr {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain B) : distrib (inr c) = _root_.Sum.inr c