Commit 2024-07-07 23:06 a0ca23aa

View on Github →

feat: define topology on DomMulAct _ (#14493)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Constructions/DomMulAct.lean

added theorem DomMulAct.closedEmbedding_mk

added theorem DomMulAct.closedEmbedding_mk_symm

added theorem DomMulAct.coe_mkHomeomorph

added theorem DomMulAct.coe_mkHomeomorph_symm

added theorem DomMulAct.comap_mk.symm_nhds

added theorem DomMulAct.comap_mk_nhds

added theorem DomMulAct.continuous_mk

added theorem DomMulAct.continuous_mk_symm

added theorem DomMulAct.embedding_mk

added theorem DomMulAct.embedding_mk_symm

added theorem DomMulAct.inducing_mk

added theorem DomMulAct.inducing_mk_symm

added theorem DomMulAct.map_mk_nhds

added theorem DomMulAct.map_mk_symm_nhds

added def DomMulAct.mkHomeomorph

added theorem DomMulAct.openEmbedding_mk

added theorem DomMulAct.openEmbedding_mk_symm

added theorem DomMulAct.quotientMap_mk

added theorem DomMulAct.quotientMap_mk_symm

Modified Mathlib/Topology/Separation.lean

added theorem Embedding.t25Space