Theorem ContinuousMap.compactOpen_eq_infₛ_induced

Modification history

2023-05-14 07:05
Mathlib/Topology/CompactOpen.lean
chore: Rename to `sSup`/`iSup` (#3938) …
Deleted ContinuousMap.compactOpen_eq_infₛ_inducedView on Github →
2023-02-11 09:23
Mathlib/Topology/CompactOpen.lean
feat: port Topology.CompactOpen (#2123)
Added ContinuousMap.compactOpen_eq_infₛ_inducedView on Github →