Commit 2024-01-30 16:07 b660fcb4

View on Github →

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

Use explicit (g : C(Y, Z)) argument instead of variable. This way only implicit arguments are not visible right there in the source.
Add dot-notation lemmas about composition of bundled continuous functions.

Estimated changes

Modified Mathlib/Topology/CompactOpen.lean

added theorem Continuous.compCM

modified theorem ContinuousMap.continuous.comp'

modified theorem ContinuousMap.continuous_comp'

modified theorem ContinuousMap.continuous_comp

modified theorem ContinuousMap.embedding_comp

modified theorem ContinuousMap.inducing_comp

added theorem ContinuousOn.compCM

added theorem Filter.Tendsto.compCM