sup_of_left — Mathlib

English

If f is measurable w.r.t mα', then it is measurable w.r.t mα ⊔ mα'.

Русский

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

LaTeX

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

Lean4

theorem sup_of_left {mα mα' : MeasurableSpace α} {_ : MeasurableSpace β} {f : α → β} (h : Measurable[mα] f) :
    Measurable[mα ⊔ mα'] f :=
  h.mono le_sup_left le_rfl

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