mk — Mathlib · SciLib

English

The mk construction is defined for AE Kolmogorov processes to yield a process Y that is an AE modification with the same properties.

Русский

Конструкция mk применяется к AEKolmogorov-процессам для получения процесса Y, являющегося AE-модификацией с теми же свойствами.

LaTeX

$$$IsAEKolmogorovProcess.mk\\ X\\ P\\ p\\ q\\ M$$$

Lean4

/-- A process with the property `IsKolmogorovProcess` such that `∀ t, X t =ᵐ[P] h.mk X t`. -/
protected noncomputable def mk (X : T → Ω → E) (h : IsAEKolmogorovProcess X P p q M) : T → Ω → E :=
  Classical.choose h

Похожие утверждения