noncomputable instance
OmegaCompletePartialOrder.Option.instOption_quasiBorelSpaces
{A : Type u_1}
[OmegaCompletePartialOrder A]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
OmegaCompletePartialOrder.Option.ωScottContinuous_some
{A : Type u_1}
[OmegaCompletePartialOrder A]
{B : Type u_2}
[OmegaCompletePartialOrder B]
{f : A → B}
(hf : ωScottContinuous f)
:
ωScottContinuous fun (x : A) => some (f x)
theorem
OmegaCompletePartialOrder.Option.ωScottContinuous_elim
{A : Type u_1}
[OmegaCompletePartialOrder A]
{B : Type u_2}
{C : Type u_3}
[OmegaCompletePartialOrder B]
[OmegaCompletePartialOrder C]
[OrderBot C]
{f : A → Option B}
(hf : ωScottContinuous f)
{g : C}
(hg : g = ⊥ := by rfl)
{h : A → B → C}
(hh : ωScottContinuous fun (x : A × B) => h x.1 x.2)
:
ωScottContinuous fun (x : A) => (f x).elim g (h x)
theorem
OmegaCompletePartialOrder.Option.ωScottContinuous_map
{A : Type u_1}
[OmegaCompletePartialOrder A]
{B : Type u_2}
{C : Type u_3}
[OmegaCompletePartialOrder B]
[OmegaCompletePartialOrder C]
{f : A → B → C}
(hf :
ωScottContinuous fun (x : A × B) =>
match x with
| (x, y) => f x y)
{g : A → Option B}
(hg : ωScottContinuous g)
:
ωScottContinuous fun (x : A) => Option.map (f x) (g x)
theorem
OmegaCompletePartialOrder.Option.ωScottContinuous_bind
{A : Type u_1}
[OmegaCompletePartialOrder A]
{B : Type u_2}
{C : Type u_3}
[OmegaCompletePartialOrder B]
[OmegaCompletePartialOrder C]
{f : A → B → Option C}
(hf :
ωScottContinuous fun (x : A × B) =>
match x with
| (x, y) => f x y)
{g : A → Option B}
(hg : ωScottContinuous g)
:
ωScottContinuous fun (x : A) => (g x).bind (f x)
theorem
OmegaCompletePartialOrder.Option.ωScottContinuous_bind'
{A : Type u_1}
[OmegaCompletePartialOrder A]
{B : Type u_2}
[OmegaCompletePartialOrder B]
{C : Type u_2}
[OmegaCompletePartialOrder C]
{f : A → B → Option C}
(hf :
ωScottContinuous fun (x : A × B) =>
match x with
| (x, y) => f x y)
{g : A → Option B}
(hg : ωScottContinuous g)
:
ωScottContinuous fun (x : A) => g x >>= f x