Constructions

📁 Source: Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean

Statistics

Metric	Count
Definitions instPseudoMetricSpace, comapPseudoMetricSpace, instPseudoMetricSpace, pseudoMetricSpaceMax, induced, pseudoMetricSpace, comapPseudoMetricSpace, instPseudoMetricSpace, instPseudoMetricSpaceNNReal	9
Theorems dist_op, dist_unop, nndist_op, nndist_unop, dist, nndist, dist, nndist, dist_op, dist_unop, nndist_op, nndist_unop, ball_zero_eq_Ico, ball_zero_eq_Ico', closedBall_zero_eq_Icc, closedBall_zero_eq_Icc', dist_eq, le_add_nndist, nndist_eq, nndist_zero_eq_val, nndist_zero_eq_val', dist_eq, dist_eq, image_ball, image_closedBall, nndist_eq, preimage_ball, preimage_closedBall, dist_eq, dist_up_up, nndist_eq, nndist_up_up, dist, nndist, ball_prod_same, closedBall_prod_same, continuous_dist, continuous_iff_continuous_dist, continuous_nndist, dist_prod_same_left, dist_prod_same_right, sphere_prod, uniformContinuous_dist, uniformContinuous_nndist	44
Total	53

AddOpposite

Definitions

Name	Category	Theorems
instPseudoMetricSpace 📖	CompOp	5 math math: nndist_op, dist_unop, dist_op, lipschitzAdd, nndist_unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_op 📖	mathematical	—	Dist.dist AddOpposite PseudoMetricSpace.toDist instPseudoMetricSpace op	—	—
dist_unop 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist unop AddOpposite instPseudoMetricSpace	—	—
nndist_op 📖	mathematical	—	NNDist.nndist AddOpposite PseudoMetricSpace.toNNDist instPseudoMetricSpace op	—	—
nndist_unop 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist unop AddOpposite instPseudoMetricSpace	—	—

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	comp₂ continuous_dist
nndist 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Continuous NNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal NNDist.nndist PseudoMetricSpace.toNNDist	—	comp₂ continuous_nndist

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Filter.Tendsto Real Dist.dist PseudoMetricSpace.toDist nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	comp Continuous.tendsto continuous_dist prodMk_nhds
nndist 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Filter.Tendsto NNReal NNDist.nndist PseudoMetricSpace.toNNDist nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal	—	comp Continuous.tendsto continuous_nndist prodMk_nhds

IsUniformInducing

Definitions

Name	Category	Theorems
comapPseudoMetricSpace 📖	CompOp	—

MulOpposite

Definitions

Name	Category	Theorems
instPseudoMetricSpace 📖	CompOp	9 math math: BoundedContinuousFunction.instIsCentralScalar, IsBoundedSMul.op, NormedAddGroupHom.isCentralScalar, nndist_op, dist_unop, lipschitzMul, dist_op, NonUnitalSeminormedRing.isBoundedSMulOpposite, nndist_unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_op 📖	mathematical	—	Dist.dist MulOpposite PseudoMetricSpace.toDist instPseudoMetricSpace op	—	—
dist_unop 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist unop MulOpposite instPseudoMetricSpace	—	—
nndist_op 📖	mathematical	—	NNDist.nndist MulOpposite PseudoMetricSpace.toNNDist instPseudoMetricSpace op	—	—
nndist_unop 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist unop MulOpposite instPseudoMetricSpace	—	—

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball_zero_eq_Ico 📖	mathematical	—	Metric.ball NNReal instPseudoMetricSpaceNNReal instZero Set.Ico PartialOrder.toPreorder instPartialOrder Real.toNNReal	—	LT.lt.le sup_of_le_left ball_zero_eq_Ico' Set.Ico_eq_empty
ball_zero_eq_Ico' 📖	mathematical	—	Metric.ball NNReal instPseudoMetricSpaceNNReal instZero toReal Set.Ico PartialOrder.toPreorder instPartialOrder	—	Set.ext nndist_zero_eq_val'
closedBall_zero_eq_Icc 📖	mathematical	Real Real.instLE Real.instZero	Metric.closedBall NNReal instPseudoMetricSpaceNNReal instZero Set.Icc PartialOrder.toPreorder instPartialOrder Real.toNNReal	—	sup_of_le_left closedBall_zero_eq_Icc'
closedBall_zero_eq_Icc' 📖	mathematical	—	Metric.closedBall NNReal instPseudoMetricSpaceNNReal instZero toReal Set.Icc PartialOrder.toPreorder instPartialOrder	—	Set.ext nndist_zero_eq_val'
dist_eq 📖	mathematical	—	Dist.dist NNReal PseudoMetricSpace.toDist instPseudoMetricSpaceNNReal abs Real Real.lattice Real.instAddGroup Real.instSub toReal	—	—
le_add_nndist 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring NNDist.nndist PseudoMetricSpace.toNNDist instPseudoMetricSpaceNNReal	—	sub_le_iff_le_add' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_abs_le Eq.ge dist_eq coe_le_coe coe_add coe_nndist
nndist_eq 📖	mathematical	—	NNDist.nndist NNReal PseudoMetricSpace.toNNDist instPseudoMetricSpaceNNReal SemilatticeSup.toMax instSemilatticeSup instSub	—	eq_of_forall_ge_iff tsub_le_iff_right Real.instIsOrderedAddMonoid AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
nndist_zero_eq_val 📖	mathematical	—	NNDist.nndist NNReal PseudoMetricSpace.toNNDist instPseudoMetricSpaceNNReal instZero	—	nndist_eq zero_tsub tsub_zero max_eq_right
nndist_zero_eq_val' 📖	mathematical	—	NNDist.nndist NNReal PseudoMetricSpace.toNNDist instPseudoMetricSpaceNNReal instZero	—	nndist_comm nndist_zero_eq_val

Prod

Definitions

Name	Category	Theorems
pseudoMetricSpaceMax 📖	CompOp	12 math math: MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_prod, sphere_prod, prod_properSpace, dist_eq, lipschitz_with_lipschitz_const_mul, dist_prod_same_left, closedBall_prod_same, dist_prod_same_right, ball_prod_same, instIsBoundedSMul, IsUnifLocDoublingMeasure.prod, lipschitz_with_lipschitz_const_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_eq 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist pseudoMetricSpaceMax Real Real.instMax	—	—

PseudoMetricSpace

Definitions

Name	Category	Theorems
induced 📖	CompOp	2 math math: isometry_induced, WithAbs.pseudoMetricSpace_induced_of_comp

Subtype

Definitions

Name	Category	Theorems
pseudoMetricSpace 📖	CompOp	82 math math: Unitary.openPartialHomeomorph_source, Metric.PiNatEmbed.continuous_distDenseSeq_inv, AffineIsometryEquiv.ofTop_apply, Unitary.continuousOn_argSelfAdjoint, Submodule.starProjection_singleton, EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq, polynomialFunctions.starClosure_topologicalClosure, LinearMap.IsSymmetric.directSum_decompose_apply, Submodule.reflection_singleton_apply, InnerProductSpace.gramSchmidt_def, Submodule.orthogonalProjection_bot, EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq, AffineSubspace.coe_subtypeₐᵢ, Submonoid.lipschitzMul, FiniteDimensional.RCLike.properSpace_submodule, EuclideanGeometry.dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq, continuousMap_mem_polynomialFunctions_closure, Submodule.reflection_orthogonalComplement_singleton_eq_neg, LinearIsometryEquiv.reflections_generate_dim_aux, Affine.Triangle.dist_circumcenter_reflection_orthocenter, preimage_ball, AffineIsometryEquiv.coe_ofEq_apply, AffineSubspace.isometryEquivMap.toAffineMap_eq, LinearIsometryEquiv.reflections_generate, AffineIsometryEquiv.ofTop_symm_apply_coe, AffineIsometryEquiv.ofEq_symm, Submodule.linearEquiv_det_reflection, stereoToFun_apply, IsUltrametricDist.subtype, AffineSubspace.toContinuousAffineMap_subtypeₐᵢ, Affine.Triangle.dist_orthocenter_reflection_circumcenter, dist_eq, Submodule.smul_starProjection_singleton, Submodule.starProjection_bot, EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq, Submodule.starProjection_unit_singleton, Submodule.reflection_sub, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, preimage_closedBall, PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice, AffineSubspace.isometryEquivMap.coe_apply, InnerProductSpace.gramSchmidt_def', Unitary.openPartialHomeomorph_target, EuclideanGeometry.eq_or_eq_reflection_of_dist_eq, Valued.integer.coe_span_singleton_eq_closedBall, Submodule.det_reflection, AffineSubspace.subtypeₐᵢ_linear, image_closedBall, MeasureTheory.Measure.toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball, nndist_eq, MeasureTheory.Lp.simpleFunc.isBoundedSMul, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, Submodule.reflection_bot, Unitary.isPathConnected_ball, Submodule.starProjection_orthogonalComplement_singleton_eq_zero, EuclideanGeometry.hasFDerivAt_inversion, AffineSubspace.signedInfDist_singleton, AffineSubspace.subtypeₐᵢ_linearIsometry, AffineIsometryEquiv.ofEq_rfl, AddSubmonoid.lipschitzAdd, LinearIsometryEquiv.reflections_generate_dim, Irreducible.maximalIdeal_eq_closedBall, stereographic_apply, polynomialFunctions.topologicalClosure, AffineSubspace.isometryEquivMap.apply_symm_apply, Irreducible.maximalIdeal_pow_eq_closedBall_pow, ContinuousMap.elemental_id_eq_top, MeasureTheory.Measure.toSphereBallBound_mul_measure_unitBall_le_toSphere_ball, polynomialFunctions_closure_eq_top', unitary.isPathConnected_ball, ProperSpace.of_isClosed, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, polynomialFunctions_closure_eq_top, AffineSubspace.subtypeₐᵢ_toAffineMap, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero, LinearMap.exists_map_addHaar_eq_smul_addHaar', instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace, image_ball, unitary.continuousOn_argSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_eq 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist pseudoMetricSpace	—	—
image_ball 📖	mathematical	—	Set.image Metric.ball pseudoMetricSpace Set Set.instInter setOf	—	preimage_ball Set.image_preimage_eq_inter_range range_val_subtype
image_closedBall 📖	mathematical	—	Set.image Metric.closedBall pseudoMetricSpace Set Set.instInter setOf	—	preimage_closedBall Set.image_preimage_eq_inter_range range_val_subtype
nndist_eq 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist pseudoMetricSpace	—	—
preimage_ball 📖	mathematical	—	Set.preimage Metric.ball pseudoMetricSpace	—	—
preimage_closedBall 📖	mathematical	—	Set.preimage Metric.closedBall pseudoMetricSpace	—	—

Topology.IsInducing

Definitions

Name	Category	Theorems
comapPseudoMetricSpace 📖	CompOp	1 math math: Topology.IsEmbedding.to_isometry

ULift

Definitions

Name	Category	Theorems
instPseudoMetricSpace 📖	CompOp	4 math math: nndist_up_up, dist_eq, nndist_eq, dist_up_up

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_eq 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist instPseudoMetricSpace	—	—
dist_up_up 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist instPseudoMetricSpace	—	—
nndist_eq 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist instPseudoMetricSpace	—	—
nndist_up_up 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist instPseudoMetricSpace	—	—

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	UniformContinuous PseudoMetricSpace.toUniformSpace	UniformContinuous Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	comp uniformContinuous_dist prodMk
nndist 📖	mathematical	UniformContinuous PseudoMetricSpace.toUniformSpace	UniformContinuous NNReal PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal NNDist.nndist PseudoMetricSpace.toNNDist	—	comp uniformContinuous_nndist prodMk

(root)

Definitions

Name	Category	Theorems
instPseudoMetricSpaceNNReal 📖	CompOp	109 math math: MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed, thickenedIndicator_mono_infEDist, MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator, BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub, MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply, thickenedIndicator_one_of_mem_closure, NNReal.tendsto_dist_agmSequences_atTop_zero, MeasureTheory.FiniteMeasure.zero_testAgainstNN, NNReal.isBoundedSMul, nndist_nnnorm_nnnorm_le_nnnorm_inv_mul, MeasureTheory.ProbabilityMeasure.continuous_lintegral_boundedContinuousFunction, NNReal.dist_agmSequences_fst_snd, thickenedIndicator_zero, MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN, HasOuterApproxClosed.tendsto_apprSeq, MeasureTheory.FiniteMeasure.testAgainstNN_const, thickenedIndicator_le_one, MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto, MeasureTheory.integrable_thickenedIndicator, BoundedContinuousFunction.lintegral_lt_top_of_nnreal, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto, NNReal.isEmbedding_coe, NNReal.closedBall_zero_eq_Icc, NNReal.hasLipschitzAdd, Metric.uniformContinuous_infNndist_pt, lipschitzWith_thickenedIndicator, MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq, NNReal.isClosedEmbedding_coe, uniformContinuous_nndist, MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegral, MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator, HasOuterApproxClosed.measure_le_lintegral, indicator_le_thickenedIndicator, BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg, isClosedMap_nndist, NNReal.le_add_nndist, BoundedContinuousFunction.nnrealPart_coeFn_eq, NNReal.instIsOrderBornology, MeasureTheory.FiniteMeasure.testAgainstNN_add, Filter.Tendsto.nndist, measure_le_lintegral_thickenedIndicator, one_le_thickenedIndicator_apply', nndist_nnnorm_nnnorm_le_nnnorm_neg_add, MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const, MeasureTheory.FiniteMeasure.testAgainstNN_zero, thickenedIndicator_tendsto_indicator_closure, HasOuterApproxClosed.apprSeq_apply_eq_one, NNReal.nndist_eq, MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_lintegral, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply, HasOuterApproxClosed.tendsto_lintegral_apprSeq, MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN, CompletelyRegularSpace.exists_BCNN, NNReal.ball_zero_eq_Ico', thickenedIndicator_subset, thickenedIndicator_apply, nndist_nnnorm_nnnorm_le', MeasureTheory.FiniteMeasure.testAgainstNN_one, MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz, uniformContinuous_nnnorm, NNReal.instOrderTopology, thickenedIndicator_mono_infEdist, NNReal.instProperSpace, NNReal.isUniformEmbedding_coe, uniformContinuous_nnnorm', Continuous.nndist, BoundedContinuousFunction.nnnorm_coeFn_eq, BoundedContinuousFunction.toReal_lintegral_coe_eq_integral, instBoundedSubNNReal, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous, HasOuterApproxClosed.indicator_le_apprSeq, BoundedContinuousFunction.measurable_coe_ennreal_comp, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous, MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz, NNReal.ball_zero_eq_Ico, thickenedIndicator_one, MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN, NNReal.dist_eq, MeasureTheory.FiniteMeasure.testAgainstNN_smul, UniformContinuous.nndist, continuousOn_cfc_nnreal_setProd, nndist_nnnorm_nnnorm_le, NNReal.closedBall_zero_eq_Icc', NNReal.nndist_zero_eq_val', instBoundedMulNNReal, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate, MeasureTheory.tendsto_lintegral_nn_filter_of_le_const, MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN, continuousOn_cfcₙ_nnreal_setProd, continuous_nndist, one_le_thickenedIndicator_apply, HasOuterApproxClosed.apprSeq_apply_le_one, BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg, NNReal.dist_gm_am_le, HasOuterApproxClosed.exAppr, NNReal.nndist_zero_eq_val, BoundedContinuousFunction.apply_le_nndist_zero, MeasureTheory.FiniteMeasure.continuous_lintegral_boundedContinuousFunction, BoundedContinuousFunction.NNReal.upper_bound, MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto, BoundedContinuousFunction.lintegral_le_edist_mul, thickenedIndicator.coeFn_eq_comp, isProperMap_nndist, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto, thickenedIndicator_mono, BoundedContinuousFunction.integrable_of_nnreal, NNReal.instCompleteSpace, NNReal.instContinuousStar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball_prod_same 📖	mathematical	—	SProd.sprod Set Set.instSProd Metric.ball Prod.pseudoMetricSpaceMax	—	Set.ext
closedBall_prod_same 📖	mathematical	—	SProd.sprod Set Set.instSProd Metric.closedBall Prod.pseudoMetricSpaceMax	—	Set.ext
continuous_dist 📖	mathematical	—	Continuous Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	UniformContinuous.continuous uniformContinuous_dist
continuous_iff_continuous_dist 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real instTopologicalSpaceProd Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	Continuous.dist Continuous.fst' Continuous.snd' continuous_iff_continuousAt tendsto_iff_dist_tendsto_zero Continuous.tendsto' Continuous.comp Continuous.prodMk_left dist_self
continuous_nndist 📖	mathematical	—	Continuous NNReal instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal NNDist.nndist PseudoMetricSpace.toNNDist	—	UniformContinuous.continuous uniformContinuous_nndist
dist_prod_same_left 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist Prod.pseudoMetricSpaceMax	—	dist_self sup_of_le_right
dist_prod_same_right 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist Prod.pseudoMetricSpaceMax	—	dist_self sup_of_le_left
sphere_prod 📖	mathematical	—	Metric.sphere Prod.pseudoMetricSpaceMax Set Set.instUnion SProd.sprod Set.instSProd Metric.closedBall	—	lt_trichotomy Metric.sphere_eq_empty_of_neg Metric.closedBall_of_neg Set.prod_empty Set.union_self Metric.closedBall_eq_sphere_of_nonpos le_rfl closedBall_prod_same Set.ext
uniformContinuous_dist 📖	mathematical	—	UniformContinuous Real instUniformSpaceProd PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	Metric.uniformContinuous_iff Nat.instAtLeastTwoHAddOfNat half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing dist_dist_dist_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_max_left le_max_right add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le add_halves ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
uniformContinuous_nndist 📖	mathematical	—	UniformContinuous NNReal instUniformSpaceProd PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal NNDist.nndist PseudoMetricSpace.toNNDist	—	uniformContinuous_dist dist_nonneg

---

← Back to Index