mono — Mathlib

English

If μ₁ ⟂ₘ ν₁ and μ₂ ≤ μ₁ and ν₂ ≤ ν₁, then μ₂ ⟂ₘ ν₂.

Русский

Если μ₁ ⟂ₘ ν₁ и μ₂ ≤ μ₁ и ν₂ ≤ ν₁, то μ₂ ⟂ₘ ν₂.

LaTeX

$$$\\mu_1 \\perp_m \\nu_1 \\to (\\mu_2 \\le \\mu_1) \\to (\\nu_2 \\le \\nu_1) \\to \\mu_2 \\perp_m \\nu_2$$$

Lean4

theorem mono (h : μ₁ ⟂ₘ ν₁) (hμ : μ₂ ≤ μ₁) (hν : ν₂ ≤ ν₁) : μ₂ ⟂ₘ ν₂ :=
  h.mono_ac hμ.absolutelyContinuous hν.absolutelyContinuous

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