Def ContinuousMap.CompactOpen.gen

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.gen View on Github →

2023-12-30 06:21

Mathlib/Topology/CompactOpen.lean

chore(Topology/CompactOpen): rename type variables (#9328) …

Modified ContinuousMap.CompactOpen.gen View on Github →

2023-02-11 09:23

Mathlib/Topology/CompactOpen.lean

feat: port Topology.CompactOpen (#2123)

Added ContinuousMap.CompactOpen.gen View on Github →