mono_set — Mathlib

English

If s ⊆ t and f is AEMeasurable w.r.t. μ restricted to t, then f is AEMeasurable w.r.t. μ restricted to s.

Русский

Если s ⊆ t и f является AЕ-измеримой относительно μ ограниченного до t, то f а также относительно μ ограниченного до s.

LaTeX

$$$s\\\\subseteq t \\\\Rightarrow \\\\text{AEMeasurable}(f,\\\\mu\\\\restriction t) \\\\Rightarrow \\\\text{AEMeasurable}(f,\\\\mu\\\\restriction s)$$$

Lean4

theorem mono_set {s t} (h : s ⊆ t) (ht : AEMeasurable f (μ.restrict t)) : AEMeasurable f (μ.restrict s) :=
  ht.mono_measure (restrict_mono h le_rfl)

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