le_outerMeasure_compacts — Mathlib

English

Let K be a compact subset of G. Then the content μ assigns to K a value that is not larger than its outer measure: μ(K) ≤ μ.outerMeasure(K).

Русский

Пусть K — компактное подмножество G. Тогда μ(K) не превосходит μ.outerMeasure(K).

LaTeX

$$$$\\forall K \\in \\mathrm{Compacts}(G):\\mu(K) \\le \\mu.outerMeasure(K).$$$$

Lean4

theorem le_outerMeasure_compacts (K : Compacts G) : μ K ≤ μ.outerMeasure K :=
  by
  rw [Content.outerMeasure, inducedOuterMeasure_eq_iInf]
  · exact le_iInf fun U => le_iInf fun hU => le_iInf <| μ.le_innerContent K ⟨U, hU⟩
  · exact fun U hU => isOpen_iUnion hU
  · exact μ.innerContent_iUnion_nat
  · exact μ.innerContent_mono

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