Algebra

📁 Source: Mathlib/Topology/MetricSpace/Algebra.lean

Statistics

Metric	Count
Definitions Algebra, IsBoundedSMul, LipschitzAdd, C, LipschitzMul, C	6
Theorems lipschitzAdd, lipschitzAdd, uniformContinuousOn_smul, continuousSMul, dist_pair_smul', dist_smul_pair', op, toUniformContinuousConstSMul, continuousAdd, lipschitz_add, continuousMul, lipschitz_mul, lipschitzMul, hasLipschitzAdd, isBoundedSMul, instIsBoundedSMul, instIsBoundedSMul', instIsBoundedSMul, hasLipschitzAdd, isBoundedSMul, lipschitzMul, fun_mul₀, fun_mul₀_of_isBoundedUnder, fun_smul₀, fun_smul₀_of_isBoundedUnder, mul₀, mul₀_of_isBoundedUnder, smul₀, smul₀_of_isBoundedUnder, fun_mul₀, fun_mul₀_of_isBoundedUnder, fun_smul₀, fun_smul₀_of_isBoundedUnder, mul₀, mul₀_of_isBoundedUnder, smul₀, smul₀_of_isBoundedUnder, dist_pair_smul, dist_smul_pair, instIsBoundedSMulSeparationQuotient, instLipschitzAddAdditiveOfLipschitzMul, instLipschitzAddOrderDual, instLipschitzMulMultiplicativeOfLipschitzAdd, instLipschitzMulOrderDual, lipschitzWith_lipschitz_const_add_edist, lipschitzWith_lipschitz_const_mul_edist, lipschitz_with_lipschitz_const_add, lipschitz_with_lipschitz_const_mul	48
Total	54

AddOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lipschitzAdd 📖	mathematical	—	LipschitzAdd AddOpposite instPseudoMetricSpace instAddMonoid	—	LE.le.trans_eq lipschitzWith_lipschitz_const_add_edist max_comm

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lipschitzAdd 📖	mathematical	—	LipschitzAdd AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership instSetLike Subtype.pseudoMetricSpace toAddMonoid	—	lipschitzWith_lipschitz_const_add_edist

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuousOn_smul 📖	mathematical	Bornology.IsBounded Prod.instBornology PseudoMetricSpace.toBornology	UniformContinuousOn instUniformSpaceProd PseudoMetricSpace.toUniformSpace	—	subset_ball_lt Metric.uniformContinuousOn_iff_le Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo le_imp_le_of_le_of_le dist_triangle le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_pair_smul add_le_add_left covariant_swap_add_of_covariant_add dist_smul_pair mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono le_of_lt max_lt_iff Prod.dist_eq Metric.mem_ball Set.mem_of_subset_of_mem dist_nonneg mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono max_le_iff Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.cons_pos Real.instZeroLEOneClass zero_lt_one NeZero.one GroupWithZero.toNontrivial Mathlib.Meta.NormNum.isNat_le_true Mathlib.Meta.NormNum.isNat_add Nat.cast_one

IsBoundedSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	continuous_iff_continuousAt ContinuousOn.continuousAt UniformContinuousOn.continuousOn Bornology.IsBounded.uniformContinuousOn_smul Metric.isBounded_ball IsOpen.mem_nhds Metric.isOpen_ball IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
dist_pair_smul' 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.instMul	—	—
dist_smul_pair' 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.instMul	—	—
op 📖	mathematical	—	IsBoundedSMul MulOpposite MulOpposite.instPseudoMetricSpace MulOpposite.instZero	—	IsCentralScalar.op_smul_eq_smul dist_smul_pair dist_pair_smul
toUniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul PseudoMetricSpace.toUniformSpace	—	LipschitzWith.uniformContinuous lipschitzWith_iff_dist_le_mul dist_smul_pair

LipschitzAdd

Definitions

Name	Category	Theorems
C 📖	CompOp	2 math math: lipschitzWith_lipschitz_const_add_edist, lipschitz_with_lipschitz_const_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAdd 📖	mathematical	—	ContinuousAdd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	LipschitzWith.continuous lipschitzWith_lipschitz_const_add_edist
lipschitz_add 📖	mathematical	—	LipschitzWith Prod.pseudoEMetricSpaceMax PseudoMetricSpace.toPseudoEMetricSpace AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	—

LipschitzMul

Definitions

Name	Category	Theorems
C 📖	CompOp	2 math math: lipschitzWith_lipschitz_const_mul_edist, lipschitz_with_lipschitz_const_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousMul 📖	mathematical	—	ContinuousMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	LipschitzWith.continuous lipschitzWith_lipschitz_const_mul_edist
lipschitz_mul 📖	mathematical	—	LipschitzWith Prod.pseudoEMetricSpaceMax PseudoMetricSpace.toPseudoEMetricSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lipschitzMul 📖	mathematical	—	LipschitzMul MulOpposite instPseudoMetricSpace instMonoid	—	LE.le.trans_eq lipschitzWith_lipschitz_const_mul_edist max_comm

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLipschitzAdd 📖	mathematical	—	LipschitzAdd NNReal instPseudoMetricSpaceNNReal AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal	—	Real.hasLipschitzAdd lipschitzWith_lipschitz_const_add_edist
isBoundedSMul 📖	mathematical	—	IsBoundedSMul NNReal instPseudoMetricSpaceNNReal instZeroNNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id	—	dist_smul_pair Real.isBoundedSMul dist_pair_smul

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsBoundedSMul 📖	mathematical	IsBoundedSMul	pseudoMetricSpacePi instZero instSMul	—	dist_pi_le_iff mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing dist_nonneg LE.le.trans dist_smul_pair mul_le_mul_of_nonneg_left dist_le_pi_dist dist_pair_smul
instIsBoundedSMul' 📖	mathematical	IsBoundedSMul	pseudoMetricSpacePi instZero smul'	—	dist_pi_le_iff mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing dist_nonneg LE.le.trans dist_smul_pair mul_le_mul IsOrderedRing.toMulPosMono dist_le_pi_dist dist_pair_smul

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsBoundedSMul 📖	mathematical	—	IsBoundedSMul pseudoMetricSpaceMax instZero instSMul	—	max_le LE.le.trans dist_smul_pair mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_max_left dist_nonneg le_max_right dist_pair_smul

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLipschitzAdd 📖	mathematical	—	LipschitzAdd Real pseudoMetricSpace instAddMonoid	—	Nat.instAtLeastTwoHAddOfNat LipschitzWith.of_dist_le_mul add_sub_add_comm two_mul le_trans abs_add_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid add_le_add covariant_swap_add_of_covariant_add le_max_left le_max_right
isBoundedSMul 📖	mathematical	—	IsBoundedSMul Real pseudoMetricSpace instZero Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id	—	sub_zero mul_sub Eq.le abs_mul instIsOrderedRing sub_mul

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lipschitzMul 📖	mathematical	—	LipschitzMul Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike Subtype.pseudoMetricSpace toMonoid	—	lipschitzWith_lipschitz_const_mul_edist

TendstoLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_mul₀ 📖	—	TendstoLocallyUniformly PseudoMetricSpace.toUniformSpace Continuous UniformSpace.toTopologicalSpace	—	—	mul₀
fun_mul₀_of_isBoundedUnder 📖	—	TendstoLocallyUniformly PseudoMetricSpace.toUniformSpace Filter.IsBoundedUnder Real Real.instLE nhds Dist.dist PseudoMetricSpace.toDist	—	—	mul₀_of_isBoundedUnder
fun_smul₀ 📖	—	TendstoLocallyUniformly PseudoMetricSpace.toUniformSpace Continuous UniformSpace.toTopologicalSpace	—	—	smul₀
fun_smul₀_of_isBoundedUnder 📖	—	TendstoLocallyUniformly PseudoMetricSpace.toUniformSpace Filter.IsBoundedUnder Real Real.instLE nhds Dist.dist PseudoMetricSpace.toDist	—	—	smul₀_of_isBoundedUnder
mul₀ 📖	mathematical	TendstoLocallyUniformly PseudoMetricSpace.toUniformSpace Continuous UniformSpace.toTopologicalSpace	Pi.instMul	—	smul₀
mul₀_of_isBoundedUnder 📖	mathematical	TendstoLocallyUniformly PseudoMetricSpace.toUniformSpace Filter.IsBoundedUnder Real Real.instLE nhds Dist.dist PseudoMetricSpace.toDist	Pi.instMul	—	smul₀_of_isBoundedUnder
smul₀ 📖	mathematical	TendstoLocallyUniformly PseudoMetricSpace.toUniformSpace Continuous UniformSpace.toTopologicalSpace	Pi.smul'	—	smul₀_of_isBoundedUnder Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.Tendsto.dist Continuous.tendsto tendsto_const_nhds
smul₀_of_isBoundedUnder 📖	mathematical	TendstoLocallyUniformly PseudoMetricSpace.toUniformSpace Filter.IsBoundedUnder Real Real.instLE nhds Dist.dist PseudoMetricSpace.toDist	Pi.smul'	—	tendstoLocallyUniformlyOn_univ TendstoLocallyUniformlyOn.smul₀_of_isBoundedUnder nhdsWithin_univ

TendstoLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_mul₀ 📖	—	TendstoLocallyUniformlyOn PseudoMetricSpace.toUniformSpace ContinuousOn UniformSpace.toTopologicalSpace	—	—	mul₀
fun_mul₀_of_isBoundedUnder 📖	—	TendstoLocallyUniformlyOn PseudoMetricSpace.toUniformSpace Filter.IsBoundedUnder Real Real.instLE nhdsWithin Dist.dist PseudoMetricSpace.toDist	—	—	mul₀_of_isBoundedUnder
fun_smul₀ 📖	—	TendstoLocallyUniformlyOn PseudoMetricSpace.toUniformSpace ContinuousOn UniformSpace.toTopologicalSpace	—	—	smul₀
fun_smul₀_of_isBoundedUnder 📖	—	TendstoLocallyUniformlyOn PseudoMetricSpace.toUniformSpace Filter.IsBoundedUnder Real Real.instLE nhdsWithin Dist.dist PseudoMetricSpace.toDist	—	—	smul₀_of_isBoundedUnder
mul₀ 📖	mathematical	TendstoLocallyUniformlyOn PseudoMetricSpace.toUniformSpace ContinuousOn UniformSpace.toTopologicalSpace	Pi.instMul	—	smul₀
mul₀_of_isBoundedUnder 📖	mathematical	TendstoLocallyUniformlyOn PseudoMetricSpace.toUniformSpace Filter.IsBoundedUnder Real Real.instLE nhdsWithin Dist.dist PseudoMetricSpace.toDist	Pi.instMul	—	smul₀_of_isBoundedUnder
smul₀ 📖	mathematical	TendstoLocallyUniformlyOn PseudoMetricSpace.toUniformSpace ContinuousOn UniformSpace.toTopologicalSpace	Pi.smul'	—	smul₀_of_isBoundedUnder Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.Tendsto.dist tendsto_const_nhds
smul₀_of_isBoundedUnder 📖	mathematical	TendstoLocallyUniformlyOn PseudoMetricSpace.toUniformSpace Filter.IsBoundedUnder Real Real.instLE nhdsWithin Dist.dist PseudoMetricSpace.toDist	Pi.smul'	—	prodMk tendstoLocallyUniformlyOn_iff_forall_tendsto Filter.IsBoundedUnder.sup Filter.Tendsto.comp Bornology.IsBounded.uniformContinuousOn_smul Metric.isBounded_ball Filter.tendsto_inf Filter.tendsto_principal Filter.mp_mem Filter.tendsto_snd Metric.dist_mem_uniformity one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Filter.univ_mem' Mathlib.Tactic.GCongr.and_right_mono lt_imp_lt_of_le_of_le dist_triangle_left le_refl lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt

(root)

Definitions

Name	Category	Theorems
Algebra 📖	CompData	8 math math: nat_algebra_subsingleton, isEmpty_algebraRat_iff_mixedCharZero, ZMod.instSubsingletonAlgebra, NormedSpace.exp_def, EqualCharZero.nonempty_algebraRat_iff, isSplittingField_AdjoinRoot_X_pow_sub_C, int_algebra_subsingleton, Rat.algebra_rat_subsingleton
IsBoundedSMul 📖	CompData	26 math math: Matrix.frobeniusIsBoundedSMul, WithLp.isBoundedSMulSeminormedAddCommGroupToProd, Submodule.Quotient.instIsBoundedSMul, NormedSpace.toIsBoundedSMul, NNReal.isBoundedSMul, IsBoundedSMul.op, Matrix.linftyOpIsBoundedSMul, Matrix.isBoundedSMul, instIsBoundedSMulSeparationQuotient, ContinuousMultilinearMap.instIsBoundedSMul, IsBoundedSMul.of_enorm_smul_le, Real.isBoundedSMul, NonUnitalSeminormedRing.isBoundedSMul, NonUnitalSeminormedRing.isBoundedSMulOpposite, TrivSqZeroExt.instL1IsBoundedSMul, BoundedContinuousFunction.instIsBoundedSMul_1, ContinuousMap.instIsBoundedSMul, MeasureTheory.Lp.instIsBoundedSMul, MeasureTheory.Lp.simpleFunc.isBoundedSMul, IsBoundedSMul.of_nnnorm_smul_le, BoundedContinuousFunction.instIsBoundedSMul, Prod.instIsBoundedSMul, NormSMulClass.toIsBoundedSMul, IsBoundedSMul.of_norm_smul_le, UniformSpace.Completion.instIsBoundedSMul, WithLp.instProdIsBoundedSMul
LipschitzAdd 📖	CompData	8 math math: NNReal.hasLipschitzAdd, instLipschitzAddOrderDual, SeminormedAddCommGroup.to_lipschitzAdd, instLipschitzAddAdditiveOfLipschitzMul, AddSubmonoid.lipschitzAdd, BoundedContinuousFunction.instLipschitzAdd, AddOpposite.lipschitzAdd, Real.hasLipschitzAdd
LipschitzMul 📖	CompData	5 math math: Submonoid.lipschitzMul, MulOpposite.lipschitzMul, instLipschitzMulMultiplicativeOfLipschitzAdd, SeminormedCommGroup.to_lipschitzMul, instLipschitzMulOrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_pair_smul 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.instMul	—	IsBoundedSMul.dist_pair_smul'
dist_smul_pair 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.instMul	—	IsBoundedSMul.dist_smul_pair'
instIsBoundedSMulSeparationQuotient 📖	mathematical	—	IsBoundedSMul SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace SeparationQuotient.instMetricSpace SeparationQuotient.instZero SeparationQuotient.instSMul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul dist_smul_pair dist_pair_smul
instLipschitzAddAdditiveOfLipschitzMul 📖	mathematical	—	LipschitzAdd Additive instPseudoMetricSpaceAdditive Additive.addMonoid	—	LipschitzMul.lipschitz_mul
instLipschitzAddOrderDual 📖	mathematical	—	LipschitzAdd OrderDual instPseudoMetricSpaceOrderDual instAddMonoidOrderDual	—	—
instLipschitzMulMultiplicativeOfLipschitzAdd 📖	mathematical	—	LipschitzMul Multiplicative instPseudoMetricSpaceMultiplicative Multiplicative.monoid	—	LipschitzAdd.lipschitz_add
instLipschitzMulOrderDual 📖	mathematical	—	LipschitzMul OrderDual instPseudoMetricSpaceOrderDual instMonoidOrderDual	—	—
lipschitzWith_lipschitz_const_add_edist 📖	mathematical	—	LipschitzWith Prod.pseudoEMetricSpaceMax PseudoMetricSpace.toPseudoEMetricSpace LipschitzAdd.C AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	LipschitzAdd.lipschitz_add
lipschitzWith_lipschitz_const_mul_edist 📖	mathematical	—	LipschitzWith Prod.pseudoEMetricSpaceMax PseudoMetricSpace.toPseudoEMetricSpace LipschitzMul.C MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	LipschitzMul.lipschitz_mul
lipschitz_with_lipschitz_const_add 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instMul NNReal.toReal LipschitzAdd.C Prod.pseudoMetricSpaceMax	—	lipschitzWith_iff_dist_le_mul lipschitzWith_lipschitz_const_add_edist
lipschitz_with_lipschitz_const_mul 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Real.instMul NNReal.toReal LipschitzMul.C Prod.pseudoMetricSpaceMax	—	lipschitzWith_iff_dist_le_mul lipschitzWith_lipschitz_const_mul_edist

---

← Back to Index