Commit 2024-10-18 09:18 3b5cedb7

View on Github →

feat(Topology): define ContinuousEval{,Const} classes (#17319)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

deleted theorem ContinuousMultilinearMap.continuous_eval

Modified Mathlib/Analysis/ODE/PicardLindelof.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Modified Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

deleted theorem ContinuousAlternatingMap.continuous_coe_fun

deleted theorem ContinuousAlternatingMap.continuous_eval_const

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

deleted theorem ContinuousMultilinearMap.continuous_coe_fun

deleted theorem ContinuousMultilinearMap.continuous_eval_const

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

added theorem UniformConvergenceCLM.continuousEvalConst

Modified Mathlib/Topology/CompactOpen.lean

deleted theorem ContinuousMap.continuous_eval

deleted theorem ContinuousMap.continuous_eval_const

Modified Mathlib/Topology/Connected/PathConnected.lean

deleted theorem Path.continuous_eval

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

added theorem ContinuousMap.hasProd_apply

deleted theorem ContinuousMap.hasSum_apply

added theorem ContinuousMap.multipliable_apply

deleted theorem ContinuousMap.summable_apply

added theorem ContinuousMap.tprod_apply

deleted theorem ContinuousMap.tsum_apply

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

Created Mathlib/Topology/Hom/ContinuousEval.lean

added theorem ContinuousEval.of_continuous_forget

Created Mathlib/Topology/Hom/ContinuousEvalConst.lean

added theorem ContinuousEvalConst.of_continuous_forget

added theorem continuous_coeFun

Modified Mathlib/Topology/Homotopy/HSpaces.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

Modified Mathlib/Topology/Homotopy/Path.lean