Theorems · Inductive type · Lie groups
SeparatelyContinuousAdd
(M : Type u_1) → [TopologicalSpace M] → [Add M] → Prop
A type class encoding that addition is continuous in each argument. This is weaker than
ContinuousAdd.
- Defined in
- Mathlib.Topology.Algebra.Monoid.Defs
- Cited by
- 83 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- TopologicalSpaceAdd
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
Cited by93
Results whose statement or proof uses this declaration.
- Continuous.const_addstatement and proof · cited by 26
- continuous_const_addstatement and proof · cited by 23
- Homeomorph.addLeftstatement and proof · cited by 20
- Homeomorph.addRightstatement and proof · cited by 18
- continuous_add_conststatement and proof · cited by 14
- Filter.Tendsto.const_addstatement and proof · cited by 12
- Continuous.add_conststatement and proof · cited by 11
- Filter.Tendsto.add_conststatement and proof · cited by 10
- ContinuousMap.addRightstatement and proof · cited by 8
- ContinuousOn.const_addstatement and proof · cited by 7
- AddSubmonoid.topologicalClosurestatement and proof · cited by 6
- discreteTopology_iff_isOpen_singleton_zerostatement and proof · cited by 6