Theorem ContinuousMap.continuous_comp'

Modification history

2024-01-30 16:07

Mathlib/Topology/CompactOpen.lean

feat(Topology/CompactOpen): add `Tendsto.compCM` etc (#9882) …

Modified ContinuousMap.continuous_comp'View on Github →

2023-12-30 06:21

Mathlib/Topology/CompactOpen.lean

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

Modified ContinuousMap.continuous_comp'View on Github →

2023-12-26 07:50

Mathlib/Topology/CompactOpen.lean

feat(CompactOpen): unify 2 `continuous_eval` lemmas (#9264) …

Modified ContinuousMap.continuous_comp'View on Github →

2023-02-11 09:23

Mathlib/Topology/CompactOpen.lean

feat: port Topology.CompactOpen (#2123)

Added ContinuousMap.continuous_comp'View on Github →