Theorem ContinuousMap.nhds_compactOpen_eq_infₛ_nhds_induced

Modification history

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