Commit 2024-10-26 04:02 e91cdbcf

View on Github →

chore(ContinuousMap): move compRight* (#17935) Also drop some unneeded assumptions and rename/deprecate some lemmas.

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

modified theorem ContinuousMap.continuous_toNNReal

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Modified Mathlib/Topology/CompactOpen.lean

added def ContinuousMap.compRightContinuousMap

added def ContinuousMap.compRightHomeomorph

deleted theorem ContinuousMap.continuous_comp

deleted theorem ContinuousMap.continuous_comp_left

added theorem ContinuousMap.continuous_postcomp

added theorem ContinuousMap.continuous_precomp

deleted theorem ContinuousMap.embedding_comp

added theorem ContinuousMap.embedding_postcomp

deleted theorem ContinuousMap.inducing_comp

added theorem ContinuousMap.inducing_postcomp

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

added theorem ContinuousMap.compRightAlgHom_continuous

Modified Mathlib/Topology/ContinuousMap/Compact.lean

deleted theorem ContinuousMap.compRightAlgHom_continuous

deleted def ContinuousMap.compRightContinuousMap

deleted theorem ContinuousMap.compRightContinuousMap_apply

deleted def ContinuousMap.compRightHomeomorph

Modified Mathlib/Topology/ContinuousMap/Sigma.lean

Modified Mathlib/Topology/ContinuousMap/Weierstrass.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean