Def ContinuousMap.ofClass

Modification history

2026-10-17 10:55

Mathlib/Topology/ContinuousMap/Defs.lean

chore: rename `toContinuousMap` to `ContinuousMap.ofClass` (#44877) …

Added ContinuousMap.ofClass View on Github →