le — Mathlib · SciLib

English

If m ≤ m0 are measurable spaces and f is measurable w.r.t m, then f is measurable w.r.t m0.

Русский

Если $\\mathcal{F} \\le \\mathcal{F}_0$ и $f$ измеримо относительно $\\mathcal{F}$, то $f$ измеримо относительно $\\mathcal{F}_0$.

LaTeX

$$$m \\le m_0 \\Rightarrow (\\forall f: \\alpha \\to \\beta, \\text{Measurable}_m f \\Rightarrow \\text{Measurable}_{m_0} f).$$$

Lean4

theorem le {α} {m m0 : MeasurableSpace α} {_ : MeasurableSpace β} (hm : m ≤ m0) {f : α → β} (hf : Measurable[m] f) :
    Measurable[m0] f := fun _ hs => hm _ (hf hs)

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