Theorems · Inductive type · Lie groups

ContinuousAddEquiv

(G : Type u) → [TopologicalSpace G] → (H : Type v) → [TopologicalSpace H] → [Add G] → [Add H] → Type (max u v)

The structure of two-sided continuous isomorphisms between additive groups. Note that both the map and its inverse have to be continuous.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

61 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceAddAdd