le_ofFunction — Mathlib

English

If f is injective, then pushing forward the outer measure of function m via f equals the outer measure built from the pullback m on preimages.

Русский

Если f инъективна, то образующая мера внешняя мера через f равна мере, построенной из m на обратных образах.

LaTeX

$$$\\text{map } f\\; (OuterMeasure.ofFunction m m\\_empty) = OuterMeasure.ofFunction (\\lambda s. m (f^{-1}[s])) m\\_empty.$$$

Lean4

theorem le_ofFunction {μ : OuterMeasure α} : μ ≤ OuterMeasure.ofFunction m m_empty ↔ ∀ s, μ s ≤ m s :=
  ⟨fun H s => le_trans (H s) (ofFunction_le s), fun H _ =>
    le_iInf fun f =>
      le_iInf fun hs => le_trans (μ.mono hs) <| le_trans (measure_iUnion_le f) <| ENNReal.tsum_le_tsum fun _ => H _⟩

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