Commit 2024-11-04 10:43 bbf4a0d7

View on Github →

feat(Topology/ContinuousMap/*): add some simp lemmas (#18326) This PR adds some easy lemmas about ContinuousMap and its relatives, intended to be used by simp.

Estimated changes

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

added theorem ContinuousMap.coe_smul'

added theorem ContinuousMap.smul_apply'

Modified Mathlib/Topology/ContinuousMap/Compact.lean

added theorem ContinuousMap.nnnorm_eq_iSup_nnnorm

added theorem ContinuousMap.nnnorm_smul_const

added theorem ContinuousMap.norm_smul_const

Modified Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean

added theorem ZeroAtInftyContinuousMap.coe_mk