Commit 2024-11-18 12:07 54d12203

View on Github →

chore: split Topology.ContinuousMap.Bounded (#19187)

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Lp/LpEquiv.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

Renamed Mathlib/Topology/ContinuousMap/Bounded.lean to Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

deleted theorem BoundedContinuousFunction.coe_star

deleted theorem BoundedContinuousFunction.star_apply

Created Mathlib/Topology/ContinuousMap/Bounded/Star.lean

added theorem BoundedContinuousFunction.coe_star

added theorem BoundedContinuousFunction.star_apply

Modified Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean

Modified Mathlib/Topology/ContinuousMap/Compact.lean

Modified Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

Modified Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

Modified Mathlib/Topology/Metrizable/Urysohn.lean

Modified Mathlib/Topology/UrysohnsBounded.lean