Topological properties of units

This file contains lemmas about the topology of units in topological monoids, including results about submonoid units and units of product spaces.

theorem Submonoid.isOpen_units {M : Type u_1} [TopologicalSpace M] [Monoid M] {U : Submonoid M} (hU : IsOpen ↑U) : IsOpen ↑U.units

If a submonoid is open in a topological monoid, then its units form an open subset of the units of the monoid.

theorem AddSubmonoid.isOpen_addUnits {M : Type u_1} [TopologicalSpace M] [AddMonoid M] {U : AddSubmonoid M} (hU : IsOpen ↑U) : IsOpen ↑U.addUnits

If a submonoid is open in a topological additive monoid, then its additive units form an open subset of the additive units of the monoid.

def ContinuousMulEquiv.piUnits {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] [(i : ι) → TopologicalSpace (M i)] : ((i : ι) → M i)ˣ ≃ₜ* ((i : ι) → (M i)ˣ)

The isomorphism of topological groups between the units of a product and the product of the units.

Equations

• ContinuousMulEquiv.piUnits = { toMulEquiv := MulEquiv.piUnits, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.piAddUnits {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] [(i : ι) → TopologicalSpace (M i)] : AddUnits ((i : ι) → M i) ≃ₜ+ ((i : ι) → AddUnits (M i))

The isomorphism of topological additive groups between the additive units of a product and the product of the additive units.

Equations

• ContinuousAddEquiv.piAddUnits = { toAddEquiv := AddEquiv.piAddUnits, continuous_toFun := ⋯, continuous_invFun := ⋯ }