Commit 2024-01-14 01:19 b40e996a

View on Github →

chore(CompactOpen): move 2 sets to variables (#9678) Also fix name in the module docs.

Estimated changes

Modified Mathlib/Topology/CompactOpen.lean

modified theorem ContinuousMap.eventually_mapsTo

modified theorem ContinuousMap.isClopen_setOf_mapsTo

modified theorem ContinuousMap.isOpen_setOf_mapsTo

modified theorem ContinuousMap.tendsto_nhds_compactOpen