Def MeasureTheory.Lp.boundedContinuousFunction

Modification history

2026-02-24 10:38
Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
chore: bump toolchain to v4.29.0-rc2 (#35708)
Deleted MeasureTheory.Lp.boundedContinuousFunctionView on Github →
2025-02-12 17:50
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
chore(MeasureTheory/Function/LpSpace.lean): split out material on (bounded) continuous functions (#21783) …
Modified MeasureTheory.Lp.boundedContinuousFunctionView on Github →
2023-05-29 08:45
Mathlib/MeasureTheory/Function/LpSpace.lean
feat: port MeasureTheory.Function.LpSpace (#4341)
Added MeasureTheory.Lp.boundedContinuousFunctionView on Github →