structure OmegaQuasiBorelSpace.Cont (R : Type u_1) (A : Type u_2) [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : Type (max u_1 u_2)

The continuation monad in the category of OmegaQuasiBorelSpaces.

• apply : (A →ω𝒒 R) →ω𝒒 R

  The underlying morphism.

theorem OmegaQuasiBorelSpace.Cont.ext {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] {x y : Cont R A} (h : x.apply = y.apply) : x = y

theorem OmegaQuasiBorelSpace.Cont.ext_iff {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] {x y : Cont R A} : x = y ↔ x.apply = y.apply

instance OmegaQuasiBorelSpace.Cont.instPartialOrder {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : PartialOrder (Cont R A)

Equations

• OmegaQuasiBorelSpace.Cont.instPartialOrder = PartialOrder.lift OmegaQuasiBorelSpace.Cont.apply ⋯

instance OmegaQuasiBorelSpace.Cont.instOmegaCompletePartialOrder {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : OmegaCompletePartialOrder (Cont R A)

Equations

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

instance OmegaQuasiBorelSpace.Cont.instQuasiBorelSpace {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : QuasiBorelSpace (Cont R A)

Equations

• OmegaQuasiBorelSpace.Cont.instQuasiBorelSpace = QuasiBorelSpace.lift OmegaQuasiBorelSpace.Cont.apply

@[simp]

theorem OmegaQuasiBorelSpace.Cont.isHom_val {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : QuasiBorelSpace.IsHom apply

theorem OmegaQuasiBorelSpace.Cont.isHom_val' {R : Type u_1} {A : Type u_2} {B : Type u_3} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] [QuasiBorelSpace B] {f : B → Cont R A} (hf : QuasiBorelSpace.IsHom f) : QuasiBorelSpace.IsHom fun (x : B) => (f x).apply

@[simp]

theorem OmegaQuasiBorelSpace.Cont.isHom_mk {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : QuasiBorelSpace.IsHom mk

theorem OmegaQuasiBorelSpace.Cont.isHom_mk' {R : Type u_1} {A : Type u_2} {B : Type u_3} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] [QuasiBorelSpace B] {f : B → (A →ω𝒒 R) →ω𝒒 R} (hf : QuasiBorelSpace.IsHom f) : QuasiBorelSpace.IsHom fun (x : B) => { apply := f x }

@[simp]

theorem OmegaQuasiBorelSpace.Cont.ωScottContinuous_mk {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : OmegaCompletePartialOrder.ωScottContinuous mk

theorem OmegaQuasiBorelSpace.Cont.ωScottContinuous_mk' {R : Type u_1} {A : Type u_2} {B : Type u_3} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] [OmegaCompletePartialOrder B] {f : B → (A →ω𝒒 R) →ω𝒒 R} (hf : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous fun (x : B) => { apply := f x }

@[simp]

theorem OmegaQuasiBorelSpace.Cont.ωScottContinuous_val {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : OmegaCompletePartialOrder.ωScottContinuous apply

theorem OmegaQuasiBorelSpace.Cont.ωScottContinuous_val' {R : Type u_1} {A : Type u_2} {B : Type u_3} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] [OmegaCompletePartialOrder B] {f : B → Cont R A} (hf : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous fun (x : B) => (f x).apply

instance OmegaQuasiBorelSpace.Cont.inst {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : OmegaQuasiBorelSpace (Cont R A)

Equations

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

def OmegaQuasiBorelSpace.Cont.unit {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : A →ω𝒒 Cont R A

The unit operator (i.e., pure values) for the continuation monad.

Equations

• OmegaQuasiBorelSpace.Cont.unit = { toFun := fun (x : A) => { apply := { toFun := fun (k : A →ω𝒒 R) => k x, isHom' := ⋯, ωScottContinuous' := ⋯ } }, isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelSpace.Cont.unit_coe_apply_coe {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] (x : A) (k : A →ω𝒒 R) : (unit x).apply k = k x

def OmegaQuasiBorelSpace.Cont.bind {R : Type u_1} {A : Type u_2} {B : Type u_3} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] [OmegaQuasiBorelSpace B] : (A →ω𝒒 Cont R B) →ω𝒒 Cont R A →ω𝒒 Cont R B

The bind operator (i.e., sequential composition) for the continuation monad.

Equations

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

@[simp]

theorem OmegaQuasiBorelSpace.Cont.bind_coe_coe_apply_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] [OmegaQuasiBorelSpace B] (f : A →ω𝒒 Cont R B) (x : Cont R A) (k : B →ω𝒒 R) : ((bind f) x).apply k = x.apply { toFun := fun (y : A) => (f y).apply k, isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelSpace.Cont.bind_unit {R : Type u_1} {A : Type u_2} {B : Type u_3} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] [OmegaQuasiBorelSpace B] (f : A →ω𝒒 Cont R B) (x : A) : (bind f) (unit x) = f x

@[simp]

theorem OmegaQuasiBorelSpace.Cont.unit_bind {R : Type u_1} {A : Type u_2} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] : bind unit = OmegaQuasiBorelHom.id

@[simp]

theorem OmegaQuasiBorelSpace.Cont.bind_bind {R : Type u_1} {A : Type u_2} {B : Type u_3} [OmegaQuasiBorelSpace R] [OmegaQuasiBorelSpace A] {C : Type u_4} [OmegaQuasiBorelSpace B] [OmegaQuasiBorelSpace C] (f : B →ω𝒒 Cont R C) (g : A →ω𝒒 Cont R B) : (bind f).comp (bind g) = bind ((bind f).comp g)