cylinderEvents_mono — Mathlib

English

If Δ1 is contained in Δ2, then the cylinder sigma-algebras grow accordingly: cylinderEvents(Δ1) ≤ cylinderEvents(Δ2).

Русский

Если Δ1 ⊆ Δ2, то σ-алгебры цилиндров удовлетворяют cylinderEvents(Δ1) ⊆ cylinderEvents(Δ2).

LaTeX

$$$\\Delta_1 \\subseteq \\Delta_2 \\Rightarrow \\mathrm{cylinderEvents}(\\Delta_1) \\le \\mathrm{cylinderEvents}(\\Delta_2)$$$

Lean4

@[gcongr]
theorem cylinderEvents_mono (h : Δ₁ ⊆ Δ₂) : cylinderEvents (X := X) Δ₁ ≤ cylinderEvents Δ₂ :=
  biSup_mono h

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