mono — Mathlib

English

If f is measurable with respect to mα, then it is measurable with respect to mα ⊔ mα'.

Русский

Если f измерим относительно mα, то он измерим относительно mα ⊔ mα'.

LaTeX

$$$$ \text{Measurable}_{m_\alpha} f \Rightarrow \text{Measurable}_{m_\alpha \sqcup m_\alpha'} f $$$$

Lean4

theorem mono {ma ma' : MeasurableSpace α} {mb mb' : MeasurableSpace β} {f : α → β} (hf : @Measurable α β ma mb f)
    (ha : ma ≤ ma') (hb : mb' ≤ mb) : @Measurable α β ma' mb' f := fun _t ht => ha _ <| hf <| hb _ ht

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