Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-22 22:12 6efec6bb

View on Github →

feat(topology/continuous_function): some lemmas spun off from #18392 (#18465) A few miscellaneous lemmas about continuous functions needed for my Poisson summation project. Companion mathlib4 PR (blank for now) at [#2369](https://github.com/leanprover-community/mathlib4/pull/2369).

Estimated changes

Modified src/topology/algebra/monoid.lean

added theorem continuous_map.coe_mul_left

added theorem continuous_map.coe_mul_right

Modified src/topology/continuous_function/algebra.lean

modified theorem continuous_map.coe_nat_cast

modified theorem continuous_map.coe_one

added theorem continuous_map.div_apply

added theorem continuous_map.int_cast_apply

added theorem continuous_map.inv_apply

added theorem continuous_map.mul_apply

added theorem continuous_map.nat_cast_apply

added theorem continuous_map.one_apply

added theorem continuous_map.periodic_tsum_comp_add_zsmul

added theorem continuous_map.pow_apply

added theorem continuous_map.zpow_apply

Modified src/topology/continuous_function/basic.lean

added theorem continuous_map.restrict_apply

added theorem continuous_map.restrict_apply_mk

Modified src/topology/continuous_function/bounded.lean

added theorem bounded_continuous_function.coe_comp_continuous

added theorem bounded_continuous_function.coe_restrict

added theorem bounded_continuous_function.comp_continuous_apply

added theorem bounded_continuous_function.restrict_apply

Modified src/topology/continuous_function/compact.lean

added theorem continuous_map.norm_restrict_mono_set