Theorem BoundedContinuousFunction.coe_posPart

Modification history

2025-04-04 03:49

Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

chore: split `Topology.ContinuousMap.Bounded.Basic` (#23574) …

Modified BoundedContinuousFunction.coe_posPart View on Github →

2024-03-20 10:53

Mathlib/Topology/ContinuousFunction/Bounded.lean

chore(Topology/ContinuousFunction/Bounded): Rename instances (#10780) …

Added BoundedContinuousFunction.coe_posPart View on Github →