Commit 2023-07-04 09:34 4f103b36

View on Github →

feat: generalize&merge ContinuousMap.continuous_eval_const{,'} (#5649) We had continuity of fun f : C(X, Y) ↦ f a in two cases:

X is a locally compact space;
X is a compact space and Y is a metric space. In fact, it is true in general topological spaces.

Estimated changes

Modified Mathlib/Topology/CompactOpen.lean

deleted theorem ContinuousMap.continuous_coe'

added theorem ContinuousMap.continuous_coe

deleted theorem ContinuousMap.continuous_eval_const'

added theorem ContinuousMap.continuous_eval_const

modified theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall

modified def Homeomorph.continuousMapOfUnique

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

modified theorem ContinuousMap.hasSum_apply

modified theorem ContinuousMap.periodic_tsum_comp_add_zsmul

modified theorem ContinuousMap.summable_apply

modified theorem ContinuousMap.tsum_apply

Modified Mathlib/Topology/ContinuousFunction/Compact.lean

deleted theorem ContinuousMap.continuous_coe

deleted theorem ContinuousMap.continuous_eval_const

Modified Mathlib/Topology/ContinuousFunction/Ideals.lean

modified theorem ContinuousMap.idealOfSet_closed

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

Modified Mathlib/Topology/Separation.lean

added theorem T2Space.of_injective_continuous