mono_set — Mathlib

English

If s ⊆ t and f is AEStronglyMeasurable on μ.restrict t, then f is AEStronglyMeasurable on μ.restrict s.

Русский

Если s ⊆ t и f AE‑строго измерима относительно μ.restrict t, то она AE‑строго измерима относительно μ.restrict s.

LaTeX

$$$s \\subseteq t \\Rightarrow AEStronglyMeasurable_m(f, μ.restrict t) \\Rightarrow AEStronglyMeasurable_m(f, μ.restrict s)$$$

Lean4

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

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