Basic properties of ω-complete partial orders #
This file is a placeholder for lemmas about OmegaCompletePartialOrder.
As the library grows, compatibility helpers specific to this project can
be added here.
@[simp]
theorem
OmegaCompletePartialOrder.ωScottContinuous_const
{A : Type u_1}
{B : Type u_2}
[OmegaCompletePartialOrder A]
[OmegaCompletePartialOrder B]
(x : B)
:
ωScottContinuous fun (x_1 : A) => x
theorem
OmegaCompletePartialOrder.ωScottContinuous_mk
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
[OmegaCompletePartialOrder A]
[OmegaCompletePartialOrder B]
[OmegaCompletePartialOrder C]
{f : A → B}
{g : A → C}
(hf : ωScottContinuous f)
(hg : ωScottContinuous g)
:
ωScottContinuous fun (x : A) => (f x, g x)
theorem
OmegaCompletePartialOrder.ωScottContinuous_fst
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
[OmegaCompletePartialOrder A]
[OmegaCompletePartialOrder B]
[OmegaCompletePartialOrder C]
{f : A → B × C}
(hf : ωScottContinuous f)
:
ωScottContinuous fun (x : A) => (f x).1
theorem
OmegaCompletePartialOrder.ωScottContinuous_snd
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
[OmegaCompletePartialOrder A]
[OmegaCompletePartialOrder B]
[OmegaCompletePartialOrder C]
{f : A → B × C}
(hf : ωScottContinuous f)
:
ωScottContinuous fun (x : A) => (f x).2
@[simp]
theorem
OmegaCompletePartialOrder.Measure.ωScottContinuous_lintegral
{A : Type u_1}
{B : Type u_2}
[OmegaCompletePartialOrder A]
[OmegaCompletePartialOrder B]
[MeasurableSpace B]
{f : A → B → ENNReal}
(hf₁ : ωScottContinuous fun (x : A × B) => f x.1 x.2)
(hf₂ : ∀ (a : A), Measurable (f a))
(μ : MeasureTheory.Measure B)
:
ωScottContinuous fun (x : A) => ∫⁻ (y : B), f x y ∂μ
theorem
OmegaCompletePartialOrder.ωScottContinuous_ite
{A : Type u_1}
{B : Type u_2}
[OmegaCompletePartialOrder A]
[OmegaCompletePartialOrder B]
{f : A → Prop}
(hf : ∀ {x y : A}, x ≤ y → f x = f y)
[DecidablePred f]
{g : A → B}
(hg : ωScottContinuous g)
{h : A → B}
(hh : ωScottContinuous h)
:
ωScottContinuous fun (x : A) => if f x then g x else h x