Theorem BoundedContinuousFunction.coe_to_continuous_fun

Modification history

2024-12-11 17:56
Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
chore(*): fix `initialize_simps_projections` commands (#19422) …
Deleted BoundedContinuousFunction.coe_to_continuous_funView on Github →
2023-05-21 21:51
Mathlib/Topology/ContinuousFunction/Bounded.lean
feat: port Topology.ContinuousFunction.Bounded (#4075)
Added BoundedContinuousFunction.coe_to_continuous_funView on Github →