Theorems · Inductive type · Lie groups

SeparatelyContinuousMul

(M : Type u_1) → [TopologicalSpace M] → [Mul M] → Prop

A type class encoding that addition is continuous in each argument. This is weaker than ContinuousMul.

Defined in: Mathlib.Topology.Algebra.Monoid.Defs
Cited by: 133 results in Mathlib
Foundations: Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Assumes: TopologicalSpace Mul

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Results whose statement or proof uses this declaration.