Theorem ContinuousMap.compactOpen_eq_sInf_induced

Modification history

2024-03-05 15:28

Mathlib/Topology/CompactOpen.lean

refactor(CompactOpen): redefine in terms of `Set.image2` and `Set.MapsTo` (#11053)

Deleted ContinuousMap.compactOpen_eq_sInf_induced View on Github →

2023-05-14 07:05

Mathlib/Topology/CompactOpen.lean

chore: Rename to `sSup`/`iSup` (#3938) …

Added ContinuousMap.compactOpen_eq_sInf_induced View on Github →