Commit 2025-03-12 08:53 85bfca59

View on Github →

chore: generalise AE{Strongly}Measurable.enorm to ContinuousENorm (#22798) From the Carleson project.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean

modified theorem measurable_enorm

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

Modified Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

Modified Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean