Commit 2023-12-26 07:50 6f7d92d3

View on Github →

feat(CompactOpen): unify 2 continuous_eval lemmas (#9264) Introduce a typeclass LocallyCompactPair that allows us to unify different versions of ContinuousMap.continuous_eval and similar lemmas.

Estimated changes

Modified Mathlib/Topology/CompactOpen.lean

modified theorem ContinuousMap.continuous.comp'

modified theorem ContinuousMap.continuous_comp'

added theorem ContinuousMap.continuous_compactOpen

deleted theorem ContinuousMap.continuous_eval'

added theorem ContinuousMap.continuous_eval

added theorem ContinuousMap.eventually_mapsTo

added theorem ContinuousMap.isOpen_setOf_mapsTo

added theorem ContinuousMap.tendsto_nhds_compactOpen

Modified Mathlib/Topology/Compactness/Compact.lean

added theorem IsCompact.elim_nhds_subcover_nhdsSet'

added theorem IsCompact.elim_nhds_subcover_nhdsSet

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

modified theorem exists_compact_between

added theorem exists_mem_nhdsSet_isCompact_mapsTo

Modified Mathlib/Topology/Connected/PathConnected.lean

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

Modified Mathlib/Topology/ContinuousFunction/Compact.lean

deleted theorem ContinuousMap.continuous_eval

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

Modified Mathlib/Topology/Separation.lean