mono_ac — Mathlib

English

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

Русский

Если μ₁ ⟂ₘ ν₁ и μ₂ существенно меньше μ₁, а ν₂ существенно меньше ν₁, то μ₂ ⟂ₘ ν₂.

LaTeX

$$$\\mu_1\\perp_m\\nu_1 \\to (\\mu_2 \\ll \\mu_1) \\land (\\nu_2 \\ll \\nu_1) \\to \\mu_2 \\perp_m \\nu_2$$$

Lean4

theorem mono_ac (h : μ₁ ⟂ₘ ν₁) (hμ : μ₂ ≪ μ₁) (hν : ν₂ ≪ ν₁) : μ₂ ⟂ₘ ν₂ :=
  let ⟨s, hs, h₁, h₂⟩ := h
  ⟨s, hs, hμ h₁, hν h₂⟩

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