# 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.

Equations

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

Equations
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.

Equations
• AddOpposite.opHomeomorph = { toEquiv := AddOpposite.opEquiv, continuous_toFun := , continuous_invFun := }
Instances For
@[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ᵃᵒᵖ), AddOpposite.opHomeomorph.symm a = a.unop
@[simp]
theorem MulOpposite.opHomeomorph_symm_apply {M : Type u_1} [] :
∀ (a : Mᵐᵒᵖ), MulOpposite.opHomeomorph.symm a = a.unop
@[simp]
theorem AddOpposite.opHomeomorph_apply {M : Type u_1} [] :
∀ (a : M), AddOpposite.opHomeomorph a =

MulOpposite.op as a homeomorphism.

Equations
• MulOpposite.opHomeomorph = { toEquiv := MulOpposite.opEquiv, continuous_toFun := , continuous_invFun := }
Instances For
instance AddOpposite.instT2Space {M : Type u_1} [] [] :
Equations
• =
instance MulOpposite.instT2Space {M : Type u_1} [] [] :
Equations
• =
instance AddOpposite.instDiscreteTopology {M : Type u_1} [] [] :
Equations
• =
instance MulOpposite.instDiscreteTopology {M : Type u_1} [] [] :
Equations
• =
@[simp]
theorem AddOpposite.map_op_nhds {M : Type u_1} [] (x : M) :
Filter.map AddOpposite.op (nhds x) =
@[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ᵃᵒᵖ) :
Filter.map AddOpposite.unop (nhds x) = nhds x.unop
@[simp]
theorem MulOpposite.map_unop_nhds {M : Type u_1} [] (x : Mᵐᵒᵖ) :
Filter.map MulOpposite.unop (nhds x) = nhds x.unop
@[simp]
theorem AddOpposite.comap_op_nhds {M : Type u_1} [] (x : Mᵃᵒᵖ) :
Filter.comap AddOpposite.op (nhds x) = nhds x.unop
@[simp]
theorem MulOpposite.comap_op_nhds {M : Type u_1} [] (x : Mᵐᵒᵖ) :
Filter.comap MulOpposite.op (nhds x) = nhds x.unop
@[simp]
theorem AddOpposite.comap_unop_nhds {M : Type u_1} [] (x : M) :
Filter.comap AddOpposite.unop (nhds x) =
@[simp]
theorem MulOpposite.comap_unop_nhds {M : Type u_1} [] (x : M) :
Filter.comap MulOpposite.unop (nhds x) =
instance AddUnits.instTopologicalSpaceAddUnits {M : Type u_1} [] [] :

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

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

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

Equations
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} [] [] [] :
Equations
• =
instance Units.instT2Space {M : Type u_1} [] [] [] :
Equations
• =
instance AddUnits.instDiscreteTopology {M : Type u_1} [] [] [] :
Equations
• =
instance Units.instDiscreteTopology {M : Type u_1} [] [] [] :
Equations
• =
theorem AddUnits.topology_eq_inf {M : Type u_1} [] [] :
AddUnits.instTopologicalSpaceAddUnits = TopologicalSpace.induced AddUnits.val inst✝¹ TopologicalSpace.induced (fun (u : ) => (-u)) inst✝¹
theorem Units.topology_eq_inf {M : Type u_1} [] [] :
Units.instTopologicalSpaceUnits = TopologicalSpace.induced Units.val inst✝¹ TopologicalSpace.induced (fun (u : Mˣ) => u⁻¹) inst✝¹
theorem AddUnits.embedding_val_mk' {M : Type u_3} [] [] {f : MM} (hc : ContinuousOn f {x : M | }) (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 : M | }) (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 : M | }) :

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 : M | }) :
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} [] [] :