Theorems · Theorem · measure theory

MeasureTheory.continuous_L1_toL1

∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m : MeasurableSpace α} {μ μ' : MeasureTheory.Measure α}
  (c' : ENNReal) (hc' : c' ≠ ⊤) (hμ'_le : μ' ≤ c' • μ), Continuous fun f => MeasureTheory.Integrable.toL1 ↑↑f ⋯

Auxiliary lemma for setToFun_congr_measure: the function sending f : α →₁[μ] G to f : α →₁[μ'] G is continuous when μ' ≤ c' • μ for c' ≠ ∞.

Defined in

Mathlib.MeasureTheory.Integral.SetToL1

Cited by

1 results in Mathlib

Foundations

Depth 231 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup