mono — Mathlib

English

If g is quasi-preserving from μb to μc and f is quasi-preserving from μa to μb, then g ∘ f is quasi-preserving from μa to μc.

Русский

Если g сохраняет μb к μc, а f — μa к μb, то g ∘ f сохраняет μa к μc.

LaTeX

$$QuasiMeasurePreserving g μb μc → QuasiMeasurePreserving f μa μb → QuasiMeasurePreserving (g ∘ f) μa μc$$

Lean4

@[mono]
theorem mono (ha : μa' ≪ μa) (hb : μb ≪ μb') (h : QuasiMeasurePreserving f μa μb) : QuasiMeasurePreserving f μa' μb' :=
  (h.mono_left ha).mono_right hb

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