Commit 2023-02-02 15:34 e823ef89

View on Github →

feat: port Topology.Algebra.Constructions (#2011)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Constructions.lean

added theorem MulOpposite.comap_op_nhds

added theorem MulOpposite.comap_unop_nhds

added theorem MulOpposite.continuous_op

added theorem MulOpposite.continuous_unop

added theorem MulOpposite.map_op_nhds

added theorem MulOpposite.map_unop_nhds

added def MulOpposite.opHomeomorph

added theorem Units.continuous_coe_inv

added theorem Units.continuous_embedProduct

added theorem Units.continuous_val

added theorem Units.embedding_embedProduct

added theorem Units.inducing_embedProduct