le_smul_caratheodory — Mathlib

English

Multiplying an outer measure by a nonnegative scalar preserves Carathéodory measurability.

Русский

Умножение внешней меры на неотрицательный скаляр сохраняет карatheодory-измеримость.

LaTeX

$$∀ a, (m : OuterMeasure α)) : m.caratheodory ≤ (a • m).caratheodory$$

Lean4

theorem le_smul_caratheodory (a : ℝ≥0∞) (m : OuterMeasure α) : m.caratheodory ≤ (a • m).caratheodory := fun s h t =>
  by
  simp only [smul_apply, smul_eq_mul]
  rw [(isCaratheodory_iff m).mp h t]
  simp [mul_add]

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