le_liftLinear_apply — Mathlib

English

For linear maps f and f1 that are equal μ-almost everywhere, the corresponding lifted maps are equal as measures on μ.

Русский

Для f и f1, равных μ-почти где-то, соответствующие поднятые отображения равны как меры на μ.

LaTeX

$$Eq (liftLinear f hf) μ = (liftLinear f1 hf1) μ$$

Lean4

theorem le_liftLinear_apply {f : OuterMeasure α →ₗ[ℝ≥0∞] OuterMeasure β} (hf) (s : Set β) :
    f μ.toOuterMeasure s ≤ liftLinear f hf μ s :=
  le_toMeasure_apply _ (hf μ) s

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