Theorem MeasureTheory.Lp.boundedContinuousFunction_topologicalClosure

Modification history

2024-05-27 23:23
Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
chore(ContinuousMapDense): reformulate using `Dense` (#13251) …
Added MeasureTheory.Lp.boundedContinuousFunction_topologicalClosureView on Github →