Theorems · Inductive type · Lie groups

ContinuousSub

(G : Type u_4) → [TopologicalSpace G] → [Sub G] → Prop

A typeclass saying that p : G × G ↦ p.1 - p.2 is a continuous function. This property automatically holds for topological additive groups but it also holds, e.g., for ℝ≥0.

Defined in

Mathlib.Topology.Algebra.Group.Defs

Cited by

48 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceSub