liftLinear_apply — Mathlib

English

If two linear maps f and g agree μ-almost everywhere, then the corresponding liftLinear maps agree as measures on μ.

Русский

Если f и g согласованы μ-почти где-то, то соответствующие liftLinear согласованы как меры на μ.

LaTeX

$$$(liftLinear f hf)_{μ} = (liftLinear g hg)_{μ}$ a.e. for μ$$

Lean4

@[simp]
theorem liftLinear_apply {f : OuterMeasure α →ₗ[ℝ≥0∞] OuterMeasure β} (hf) {s : Set β} (hs : MeasurableSet s) :
    liftLinear f hf μ s = f μ.toOuterMeasure s :=
  toMeasure_apply _ (hf μ) hs

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