# Documentation

Mathlib.Topology.Algebra.Constructions

# Topological space structure on the opposite monoid and on the units group #

In this file we define TopologicalSpace structure on Mᵐᵒᵖ, Mᵃᵒᵖ, Mˣ, and AddUnits M. This file does not import definitions of a topological monoid and/or a continuous multiplicative action, so we postpone the proofs of HasContinuousMul Mᵐᵒᵖ etc till we have these definitions.

## Tags #

topological space, opposite monoid, units

Put the same topological space structure on the opposite monoid as on the original space.

Put the same topological space structure on the opposite monoid as on the original space.

theorem AddOpposite.continuous_unop {M : Type u_1} [] :
theorem MulOpposite.continuous_unop {M : Type u_1} [] :
Continuous MulOpposite.unop
theorem AddOpposite.continuous_op {M : Type u_1} [] :
theorem MulOpposite.continuous_op {M : Type u_1} [] :
Continuous MulOpposite.op

AddOpposite.op as a homeomorphism.

Instances For
@[simp]
theorem MulOpposite.opHomeomorph_symm_apply {M : Type u_1} [] :
∀ (a : Mᵐᵒᵖ), ↑(Homeomorph.symm MulOpposite.opHomeomorph) a =
@[simp]
theorem AddOpposite.opHomeomorph_apply {M : Type u_1} [] :
∀ (a : M), AddOpposite.opHomeomorph a =
@[simp]
theorem MulOpposite.opHomeomorph_apply {M : Type u_1} [] :
∀ (a : M), MulOpposite.opHomeomorph a =
@[simp]
theorem AddOpposite.opHomeomorph_symm_apply {M : Type u_1} [] :
∀ (a : Mᵃᵒᵖ), ↑(Homeomorph.symm AddOpposite.opHomeomorph) a =

MulOpposite.op as a homeomorphism.

Instances For
instance AddOpposite.instT2Space {M : Type u_1} [] [] :
instance MulOpposite.instT2Space {M : Type u_1} [] [] :
instance AddOpposite.instDiscreteTopology {M : Type u_1} [] [] :
instance MulOpposite.instDiscreteTopology {M : Type u_1} [] [] :
@[simp]
theorem AddOpposite.map_op_nhds {M : Type u_1} [] (x : M) :
@[simp]
theorem MulOpposite.map_op_nhds {M : Type u_1} [] (x : M) :
Filter.map MulOpposite.op (nhds x) =
@[simp]
theorem AddOpposite.map_unop_nhds {M : Type u_1} [] (x : Mᵃᵒᵖ) :
@[simp]
theorem MulOpposite.map_unop_nhds {M : Type u_1} [] (x : Mᵐᵒᵖ) :
Filter.map MulOpposite.unop (nhds x) =
@[simp]
theorem AddOpposite.comap_op_nhds {M : Type u_1} [] (x : Mᵃᵒᵖ) :
@[simp]
theorem MulOpposite.comap_op_nhds {M : Type u_1} [] (x : Mᵐᵒᵖ) :
Filter.comap MulOpposite.op (nhds x) =
@[simp]
theorem AddOpposite.comap_unop_nhds {M : Type u_1} [] (x : M) :
@[simp]
theorem MulOpposite.comap_unop_nhds {M : Type u_1} [] (x : M) :
Filter.comap MulOpposite.unop (nhds x) =

The additive units of a monoid are equipped with a topology, via the embedding into M × M.

instance Units.instTopologicalSpaceUnits {M : Type u_1} [] [] :

The units of a monoid are equipped with a topology, via the embedding into M × M.

theorem AddUnits.inducing_embedProduct {M : Type u_1} [] [] :
theorem Units.inducing_embedProduct {M : Type u_1} [] [] :
theorem Units.embedding_embedProduct {M : Type u_1} [] [] :
instance AddUnits.instT2Space {M : Type u_1} [] [] [] :
theorem AddUnits.instT2Space.proof_1 {M : Type u_1} [] [] [] :
instance Units.instT2Space {M : Type u_1} [] [] [] :
instance AddUnits.instDiscreteTopology {M : Type u_1} [] [] [] :
instance Units.instDiscreteTopology {M : Type u_1} [] [] [] :
theorem AddUnits.topology_eq_inf {M : Type u_1} [] [] :
theorem Units.topology_eq_inf {M : Type u_1} [] [] :
Units.instTopologicalSpaceUnits = TopologicalSpace.induced Units.val inst✝ TopologicalSpace.induced (fun u => u⁻¹) inst✝
theorem AddUnits.embedding_val_mk' {M : Type u_3} [] [] {f : MM} (hc : ContinuousOn f {x | }) (hf : ∀ (u : ), f u = ↑(-u)) :

An auxiliary lemma that can be used to prove that coercion AddUnits M → M is a topological embedding. Use AddUnits.embedding_val or toAddUnits_homeomorph instead.

theorem Units.embedding_val_mk' {M : Type u_3} [] [] {f : MM} (hc : ContinuousOn f {x | }) (hf : ∀ (u : Mˣ), f u = u⁻¹) :
Embedding Units.val

An auxiliary lemma that can be used to prove that coercion Mˣ → M is a topological embedding. Use Units.embedding_val₀, Units.embedding_val, or toUnits_homeomorph instead.

theorem AddUnits.embedding_val_mk {M : Type u_3} [] (h : ContinuousOn Neg.neg {x | }) :

An auxiliary lemma that can be used to prove that coercion AddUnits M → M is a topological embedding. Use AddUnits.embedding_val or toAddUnits_homeomorph instead.

theorem Units.embedding_val_mk {M : Type u_3} [] [] (h : ContinuousOn Inv.inv {x | }) :
Embedding Units.val

An auxiliary lemma that can be used to prove that coercion Mˣ → M is a topological embedding. Use Units.embedding_val₀, Units.embedding_val, or toUnits_homeomorph instead.

theorem Units.continuous_embedProduct {M : Type u_1} [] [] :
theorem AddUnits.continuous_val {M : Type u_1} [] [] :