Theorems · Inductive type · general topology
LipschitzAdd
(β : Type u_2) → [PseudoMetricSpace β] → [AddMonoid β] → Prop
Class LipschitzAdd M says that the addition (+) : X × X → X is Lipschitz jointly in
the two arguments.
- Defined in
- Mathlib.Topology.MetricSpace.Algebra
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- PseudoMetricSpaceAddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement · cited by 2,864
- PseudoMetricSpacestatement · cited by 1,550
Cited by10
Results whose statement or proof uses this declaration.
- ContinuousMap.addEquivBoundedOfCompactstatement and proof · cited by 4
- LipschitzAdd.Cstatement and proof · cited by 2
- lipschitzWith_lipschitz_const_add_ediststatement and proof · cited by 1
- LipschitzAdd.lipschitz_addstatement and proof · cited by 1
- ContinuousMap.addEquivBoundedOfCompact_applystatement and proof · cited by 0
- ContinuousMap.addEquivBoundedOfCompact_symm_applystatement and proof · cited by 0
- LipschitzAdd.casesOnstatement and proof · cited by 0
- ContinuousMap.addEquivBoundedOfCompact.congr_simpstatement and proof · cited by 0
- LipschitzAdd.recOnstatement and proof · cited by 0
- lipschitz_with_lipschitz_const_addstatement and proof · cited by 0