Commit 2023-05-30 08:46 7e873bba

View on Github →

feat: port Topology.Algebra.ContinuousMonoidHom (#4162)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added structure ContinuousAddMonoidHom

added theorem ContinuousMonoidHom.closedEmbedding_toContinuousMap

added def ContinuousMonoidHom.comp

added def ContinuousMonoidHom.compLeft

added def ContinuousMonoidHom.compRight

added theorem ContinuousMonoidHom.continuous_comp

added theorem ContinuousMonoidHom.continuous_comp_left

added theorem ContinuousMonoidHom.continuous_comp_right

added theorem ContinuousMonoidHom.continuous_of_continuous_uncurry

added def ContinuousMonoidHom.coprod

added def ContinuousMonoidHom.diag

added theorem ContinuousMonoidHom.embedding_toContinuousMap

added theorem ContinuousMonoidHom.ext

added def ContinuousMonoidHom.fst

added def ContinuousMonoidHom.id

added theorem ContinuousMonoidHom.inducing_toContinuousMap

added def ContinuousMonoidHom.inl

added def ContinuousMonoidHom.inr

added def ContinuousMonoidHom.inv

added def ContinuousMonoidHom.mk'

added def ContinuousMonoidHom.mul

added def ContinuousMonoidHom.one

added def ContinuousMonoidHom.prod

added def ContinuousMonoidHom.prod_map

added def ContinuousMonoidHom.snd

added def ContinuousMonoidHom.swap

added def ContinuousMonoidHom.toContinuousMap

added theorem ContinuousMonoidHom.toContinuousMap_injective

added structure ContinuousMonoidHom

added theorem PontryaginDual.map_apply

added theorem PontryaginDual.map_comp

added theorem PontryaginDual.map_mul'

added theorem PontryaginDual.map_one

added def PontryaginDual