outerMeasure_le_iff — Mathlib

English

An outer measure m is bounded by μ if and only if for all measurable s, m(s) ≤ μ(s).

Русский

Внешняя мера m не превосходит μ тогда и только тогда, когда для всех измеримых s выполняется m(s) ≤ μ(s).

LaTeX

$$$m \le \mu.1 \iff \forall s\ MeasurableSet(s),\; m(s) \le \mu(s)$$$

Lean4

theorem outerMeasure_le_iff {m : OuterMeasure α} : m ≤ μ.1 ↔ ∀ s, MeasurableSet s → m s ≤ μ s := by
  simpa only [μ.trimmed] using OuterMeasure.le_trim_iff (m₂ := μ.1)

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