instance ProbNetKAT.instCompletePartialOrderProd_probNetKAT {α β : Type} [CompletePartialOrder α] [CompletePartialOrder β] : CompletePartialOrder (α × β)

Lemma 5. (i) The cartesian product of any collection of DCPOs is a DCPO under the componentwise order.

Equations

• ProbNetKAT.instCompletePartialOrderProd_probNetKAT = { toPartialOrder := Prod.instPartialOrder α β, toSupSet := Prod.supSet α β, lubOfDirected := ⋯ }

instance ProbNetKAT.instCompletePartialOrderPi {E D : Type} [CompletePartialOrder E] : CompletePartialOrder (D → E)

Lemma 5. (iii) If E is a DCPO and D is any set, then the family of functions f : D → E is a DCPO under the pointwise order f ⊑ g iff for all a ∈ D, f(a) ⊑ g(a). The supremum of a directed set D of functions D → E is the function (⨆𝒟)(a) = ⨆ f ∈ 𝒟, f(a).

Equations

• ProbNetKAT.instCompletePartialOrderPi = { toPartialOrder := Pi.partialOrder, toSupSet := Pi.supSet, lubOfDirected := ⋯ }

instance ProbNetKAT.instPartialOrderProbabilityMeasureSet_probNetKAT {H : Type} : PartialOrder (MeasureTheory.ProbabilityMeasure (Set H))

Equations

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

noncomputable def ProbNetKAT.ℬ_sSup {H : Type} (D : Set (MeasureTheory.ProbabilityMeasure (Set H))) : MeasureTheory.ProbabilityMeasure (Set H)

Equations

• ProbNetKAT.ℬ_sSup D = ⟨ProbNetKAT.measure_of_fin (fun (B : ↑ProbNetKAT.B_b_fin) => ⨆ μ ∈ D, ↑(μ ↑B)) ⋯, ⋯⟩

noncomputable instance ProbNetKAT.instCompletePartialOrderProbabilityMeasureSet_probNetKAT {H : Type} : CompletePartialOrder (MeasureTheory.ProbabilityMeasure (Set H))

Equations

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

noncomputable instance ProbNetKAT.instLE {H : Type} : LE (ProbabilityTheory.Kernel (Set H) (Set H))

Equations

• ProbNetKAT.instLE = { le := fun (a b : ProbabilityTheory.Kernel (Set H) (Set H)) => ∀ (i : Set H), ∀ B ∈ ProbNetKAT.𝒪, (a i) B ≤ (b i) B }

noncomputable instance ProbNetKAT.instPartialOrderKernelSet_probNetKAT {H : Type} : PartialOrder (ProbabilityTheory.Kernel (Set H) (Set H))

Equations

• ProbNetKAT.instPartialOrderKernelSet_probNetKAT = { toLE := ProbNetKAT.instLE, toLT := Preorder.toLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯, le_antisymm := ⋯ }