Theorem BoundedContinuousFunction.coe_toContinuousMap

Modification history

2024-12-11 17:56
Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
chore(*): fix `initialize_simps_projections` commands (#19422) …
Added BoundedContinuousFunction.coe_toContinuousMapView on Github →