hausdorffMeasure_mono — Mathlib

English

If d1 ≤ d2 then μH[d2] s ≤ μH[d1] s for all s.

Русский

Если d1 ≤ d2, то μH[d2] s ≤ μH[d1] s для всех s.

LaTeX

$$$ μH[d2] s \le μH[d1] s $$$

Lean4

/-- Hausdorff measure `μH[d] s` is monotone in `d`. -/
theorem hausdorffMeasure_mono {d₁ d₂ : ℝ} (h : d₁ ≤ d₂) (s : Set X) : μH[d₂] s ≤ μH[d₁] s :=
  by
  rcases h.eq_or_lt with (rfl | h); · exact le_rfl
  rcases hausdorffMeasure_zero_or_top h s with hs | hs
  · rw [hs]; exact zero_le _
  · rw [hs]; exact le_top

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