Defs

📁 Source: Mathlib/Topology/EMetricSpace/Defs.lean

Statistics

Metric	Count
Definitions instPseudoEMetricSpace, EDist, edist, ball, closedBall, edistLtTopSetoid, EMetricSpace, induced, replaceTopology, replaceUniformity, toPseudoEMetricSpace, closedEBall, eball, edistLtTopSetoid, instPseudoEMetricSpace, pseudoEMetricSpaceMax, PseudoEMetricSpace, induced, ofEDistOfTopology, replaceUniformity, toEDist, toUniformSpace, ofEdistOfTopology, instEDistAdditive, instEDistMultiplicative, instEDistOrderDual, instEMetricSpaceAddOpposite, instEMetricSpaceAdditive, instEMetricSpaceMulOpposite, instEMetricSpaceMultiplicative, instEMetricSpaceOrderDual, instEMetricSpaceSubtype, instEMetricSpaceULift, instPseudoEMetricSpaceAdditive, instPseudoEMetricSpaceMultiplicative, instPseudoEMetricSpaceOrderDual, instPseudoEMetricSpaceSubtype, instPseudoEMetricSpaceULift, uniformSpaceOfEDist, uniformSpaceOfEDistOfHasBasis	40
Theorems edist_op, edist_unop, ext, ext_iff, ball_disjoint, ball_eq_empty_iff, ball_mem_nhds, ball_prod_same, ball_subset, ball_subset_ball, ball_subset_closedBall, ball_zero, closedBall_mem_nhds, closedBall_prod_same, closedBall_subset_closedBall, closedBall_top, closedBall_zero, dense_iff, exists_ball_subset_ball, instIsCountablyGeneratedUniformity, isClosed_ball_top, isOpen_ball, isOpen_iff, mem_ball, mem_ball', mem_ball_comm, mem_ball_self, mem_closedBall, mem_closedBall', mem_closedBall_comm, mem_closedBall_self, mem_closure_iff, mem_nhdsWithin_iff, mem_nhds_iff, mk_uniformity_basis, mk_uniformity_basis_le, nhdsWithin_basis_closed_eball, nhdsWithin_basis_eball, nhds_basis_closed_eball, nhds_basis_eball, nhds_eq, ordConnected_setOf_ball_subset, ordConnected_setOf_closedBall_subset, pos_of_mem_ball, tendsto_atTop, tendsto_nhds, tendsto_nhdsWithin_nhds, tendsto_nhdsWithin_nhdsWithin, tendsto_nhds_nhds, uniformContinuousOn_iff, uniformContinuous_iff, eq_of_edist_eq_zero, ext, ext_iff, closedEBall_mem_nhds, closedEBall_prod_same, closedEBall_subset_closedEBall, closedEBall_top, closedEBall_zero, eball_disjoint, eball_eq_empty_iff, eball_mem_nhds, eball_prod_same, eball_subset, eball_subset_closedEBall, eball_subset_eball, eball_zero, exists_eball_subset_eball, isClosed_eball_top, isOpen_eball, mem_closedEBall, mem_closedEBall', mem_closedEBall_comm, mem_closedEBall_self, mem_eball, mem_eball', mem_eball_comm, mem_eball_self, nhdsWithin_basis_closedEBall, nhdsWithin_basis_eball, nhds_basis_closedEBall, nhds_basis_eball, ordConnected_setOf_closedEBall_subset, ordConnected_setOf_eball_subset, pos_of_mem_eball, edist_op, edist_unop, edist_eq, edist_comm, edist_self, edist_triangle, ext, ext_iff, uniformity_edist, edist_eq, edist_mk_mk, image_closedEBall, image_eball, image_emetricBall, image_emetricClosedBall, preimage_closedEBall, preimage_eball, preimage_emetricBall, preimage_emetricClosedBall, edist_eq, edist_up_up, edist_congr, edist_congr_left, edist_congr_right, edist_eq_zero, edist_le_zero, edist_mem_uniformity, edist_ofAdd, edist_ofDual, edist_ofMul, edist_pos, edist_toAdd, edist_toDual, edist_toMul, edist_triangle4, edist_triangle_left, edist_triangle_right, eq_of_forall_edist_le, mem_uniformity_edist, uniformSpace_edist, uniformity_basis_edist, uniformity_basis_edist', uniformity_basis_edist_inv_nat, uniformity_basis_edist_inv_two_pow, uniformity_basis_edist_le, uniformity_basis_edist_le', uniformity_basis_edist_nnreal, uniformity_basis_edist_nnreal_le, uniformity_dist_of_mem_uniformity, uniformity_edist, uniformity_pseudoedist, zero_eq_edist	137
Total	177

AddOpposite

Definitions

Name	Category	Theorems
instPseudoEMetricSpace 📖	CompOp	3 math math: edist_op, instIsIsometricVAddAddOpposite, edist_unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_op 📖	mathematical	—	EDist.edist AddOpposite PseudoEMetricSpace.toEDist instPseudoEMetricSpace op	—	—
edist_unop 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist unop AddOpposite instPseudoEMetricSpace	—	—

EDist

Definitions

Name	Category	Theorems
edist 📖	CompOp	390 math math: WithLp.prod_edist_eq_card, edist_eq_enorm_sub, edist_congr_left, Prod.edist_eq, eVariationOn.sum_le_of_monotoneOn_Icc, PseudoEMetricSpace.edist_comm, Set.Finite.einfsep, MeasureTheory.hausdorffMeasure_segment, WithLp.edist_fst_le, Set.einfsep_of_fintype, Metric.isSeparated_insert_of_notMem, PiLp.edist_self, LipschitzWith.edist_lt_of_edist_lt_div, edist_le_of_edist_le_geometric_two_of_tendsto₀, Set.einfsep_pair_le_left, EMetric.le_infEdist, MeasureTheory.MeasuredSets.sub_le_edist, ContractingWith.edist_le_of_fixedPoint, edist_mem_uniformity, MeasureTheory.Lp.edist_def, edist_div_right, UniformFun.edist_eval_le, Congruent.pairwise_edist_eq, edist_le_pi_edist, HolderWith.edist_le_of_le, nndist_edist, Metric.mem_closedEBall, uniformity_basis_edist, edist_zero_left, edist_le_Ico_sum_of_edist_le, MeasureTheory.LevyProkhorov.edist_measure_def, lintegral_fderiv_lineMap_eq_edist, edist_zero_eq_enorm, Metric.isSeparated_iff_setRelIsSeparated, AffineIsometryEquiv.edist_map, Metric.infEDist_le_edist_of_mem, Isometry.edist_eq, TopologicalSpace.Compacts.edist_eq, MeasureTheory.SimpleFunc.nearestPtInd_succ, EMetric.diam_pair, DilationEquiv.edist_eq', EMetric.diam_le_iff, Metric.ediam_triple, edist_le_of_edist_le_geometric_of_tendsto, Metric.PiNatEmbed.edist_def, measurable_edist_right, Set.einfsep_zero, EMetric.mem_ball, MeasureTheory.Integrable.edist_toL1_zero, Metric.infEDist_le_infEDist_add_edist, EMetric.mem_closedBall, congruent_iff_pairwise_edist_eq, Set.Finset.coe_einfsep, EMetric.exists_edist_lt_of_hausdorffEdist_lt, uniformity_basis_edist_le, EMetric.isUniformEmbedding_iff, MulOpposite.edist_op, PiCountable.min_edist_le_edist_pi, MeasureTheory.Lp.dist_edist, Set.einfsep_le_edist_of_mem, DilationClass.edist_eq', PiCountable.edist_eq_tsum, MeasureTheory.Lp.edist_eq_eLpNorm_neg_add, edist_div_left, edist_ofDual, AddOpposite.edist_op, edist_le_of_edist_le_geometric_two_of_tendsto, MeasureTheory.Lp.edist_toLp_toLp, MeasureTheory.StronglyMeasurable.edist, EMetric.diam_insert, ContractingWith.apriori_edist_iterate_efixedPoint_le', PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius, EMetric.uniformContinuous_iff, IsometryEquiv.edist_eq, MeasureTheory.Integrable.norm_toL1, edist_le_tsum_of_edist_le_of_tendsto₀, LinearIsometry.edist_map, MeasureTheory.Lp.edist_toLp_zero, edist_le_ofReal, edist_le_tsum_of_edist_le_of_tendsto, edist_neg, EMetric.cauchySeq_iff, MeasureTheory.edist_indicatorConstLp_eq_enorm, PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius, EMetric.tendsto_nhds, edist_lt_ofReal, uniformity_basis_edist_le', WithLp.edist_toLp_snd, Dilation.edist_eq', EMetric.mk_uniformity_basis_le, PiLp.edist_eq_sum, similar_iff_exists_edist_eq, Metric.isSeparated_insert, DomMulAct.edist_smul_Lp, unitInterval.volume_uIcc, MeasureTheory.lintegral_edist_triangle, variationOnFromTo.eq_zero_iff_of_le, unitInterval.volume_uIoo, WithLp.prod_edist_eq_of_L2, MulOpposite.edist_unop, EMetric.infEdist_singleton, eVariationOn.sum_le_of_monotoneOn_Iic, UniformOnFun.edist_eval_le, WithLp.prod_edist_eq_sup, MeasureTheory.lintegral_edist_lt_top, Dilation.edist_eq, MeasureTheory.LevyProkhorov.edist_finiteMeasure_def, MeasureTheory.hasFiniteIntegral_iff_edist, ContractingWith.edist_efixedPoint_lt_top', edist_mul_mul_le, edist_mul_right, continuous_edist, EMetric.controlled_of_isUniformEmbedding, PairReduction.edist_le_of_mem_pairSet, edist_sub_left, AddOpposite.edist_unop, MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_spec, Metric.ediam_eq_sSup, ContractingWith.edist_efixedPoint_le', AEMeasurable.edist, MeasureTheory.SimpleFunc.edist_approxOn_y0_le, coe_nnreal_ennreal_nndist, LipschitzWith.edist_iterate_succ_le_geometric, SeparationQuotient.edist_mk, Set.einfsep_insert, uniformity_basis_edist_inv_nat, MeasureTheory.SimpleFunc.edist_approxOn_mono, EuclideanSpace.edist_single_same, Set.einfsep_lt_iff, ProbabilityTheory.IsKolmogorovProcess.measurable_edist, Metric.mem_closedEBall', TopologicalSpace.Closeds.edist_eq, LipschitzWith.edist_le_mul, ProbabilityTheory.IsAEKolmogorovProcess.kolmogorovCondition, ProbabilityTheory.IsKolmogorovProcess.kolmogorovCondition, EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt, LipschitzOnWith.edist_lt_of_edist_lt_div, Set.einfsep_insert_le, LipschitzOnWith.edist_le_mul_of_le, Metric.le_infEDist, edist_neg_neg, Set.einfsep_top, edist_vadd_left, ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero, edist_one_right, EMetric.tendsto_nhds_nhds, Metric.edist_le_ediam_of_mem, edist_toAdd, Set.le_einfsep_iff, UniformFun.edist_le, PseudoEMetricSpace.edist_self, edist_triangle4, edist_triangle_right, edist_toMul, ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist, ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero_of_const_eq_zero, LipschitzWith.mul_edist_le, Metric.edist_le_infEDist_add_ediam, EMetric.mem_ball', LipschitzWith.edist_le_mul_of_le, Set.relatively_discrete_of_finite, EMetric.infEdist_le_edist_add_infEdist, edist_one_eq_enorm, edist_smul₀, uniformity_basis_edist_nnreal_le, Inseparable.edist_eq_zero, edist_eq_enorm_div, EMetric.isUniformEmbedding_iff', EMetric.pair_reduction, ContractingWith.exists_fixedPoint, PiLp.edist_eq_iSup, PiCountable.edist_le_edist_pi_of_edist_lt, variationOnFromTo.eq_zero_iff_of_ge, uniformity_basis_edist_inv_two_pow, EMetric.tendsto_atTop, edist_lt_coe, EMetric.edist_le_infEdist_add_ediam, edist_add_add_le, similar_iff_exists_pairwise_edist_eq, PiLp.edist_apply_le, edist_sub_right, AntilipschitzWith.edist_lt_top, eVariationOn.edist_le, Metric.mem_thickening_iff_exists_edist_lt, UniformOnFun.edist_def', EMetric.edist_le_diam_of_mem, PiCountable.edist_le_two, LinearIsometryEquiv.edist_map, EMetric.cauchySeq_iff_le_tendsto_0, MeasureTheory.LevyProkhorov.edist_probabilityMeasure_def, ContractingWith.edist_inequality, Set.Finite.relatively_discrete, measurable_edist_left, Metric.ediam_pair, MeasureTheory.L1.dist_def, Set.einfsep_lt_top, Set.einfsep_eq_iInf, edist_dist, UniformFun.edist_def, edist_le_zero, uniformity_edist, hasConstantSpeedOnWith_zero_iff, Set.einfsep_pair_eq_inf, edist_ofAdd, Set.infsep_pair_le_toReal_inf, DomAddAct.edist_vadd_Lp, EMetric.infEdist_le_edist_of_mem, edist_add_left, eVariationOn.sum_le, eVariationOn.add_point, edist_smul_left, edist_le_coe, WithLp.prod_edist_eq_of_L1, EMetric.diam_image_le_iff, Congruent.edist_eq, edist_lt_top, UniformOnFun.edist_eq_pi_restrict, Metric.Snowflaking.edist_toSnowflaking_toSnowflaking, UniformOnFun.edist_def, eventually_riemannianEDist_le_edist_extChartAt, variationOnFromTo.edist_zero_of_eq_zero, eVariationOn.eVariationOn_eq_strictMonoOn, Similar.exists_edist_eq, Metric.infEDist_singleton, WithLp.prod_edist_self, DilationEquivClass.edist_eq', Set.einfsep_pair_le_right, LipschitzWith.edist_lt_mul_of_lt, ContractingWith.exists_fixedPoint', BoundedContinuousFunction.edist_eq_iSup, ContractingWith.edist_efixedPoint_lt_top, ext_iff, PiCountable.edist_lt_top, Metric.uniformity_edist, edist_congr, EMetric.mem_closedBall', edist_mul_left, MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal, PiLp.edist_eq_card, Metric.ediam_image_le_iff, EMetric.tendsto_nhdsWithin_nhds, edist_congr_right, UniformOnFun.edist_continuousRestrict, EMetric.cauchy_iff, EMetric.uniformContinuousOn_iff, edist_le_range_sum_edist, Set.le_edist_of_le_einfsep, MeasureTheory.Egorov.mem_notConvergentSeq_iff, PiLp.edist_toLp_single_same, Set.infsep_pair_eq_toReal, edist_add_right, EMetric.mk_uniformity_basis, Set.le_einfsep_image_iff, edist_vadd_vadd_le, Metric.exists_edist_lt_of_hausdorffEDist_lt, PairReduction.exists_radius_le, Set.einfsep_triple, EMetric.mem_closure_iff, IsometryClass.edist_eq, EMetric.infEdist_lt_iff, MeasureTheory.dist_integral_le_lintegral_edist, edist_zero_right, edist_pi_le_iff, Subtype.edist_mk_mk, edist_ofMul, MeasureTheory.lintegral_enorm_eq_lintegral_edist, tendsto_iff_edist_tendsto_0, EMetric.infEdist_le_infEdist_add_edist, edist_le_of_edist_le_geometric_of_tendsto₀, Metric.Snowflaking.edist_ofSnowflaking_ofSnowflaking, Measurable.edist, edist_inv_inv, Metric.hausdorffEDist_singleton, zero_eq_edist, Set.einfsep_pair, EMetric.cauchySeq_iff_NNReal, Metric.ediam_union_le_add_edist, variationOnFromTo.eq_zero_iff, edist_pi_const_le, edist_pi_def, MeasureTheory.hausdorffMeasure_affineSegment, IsCompact.exists_infEdist_eq_edist, Set.le_einfsep_pair, AffineIsometry.edist_map, ULift.edist_up_up, ContractingWith.eq_or_edist_eq_top_of_fixedPoints, Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt, HolderOnWith.edist_le, EMetric.tendsto_nhdsWithin_nhdsWithin, edist_inv, Metric.Snowflaking.edist_def, WithLp.edist_toLp_fst, Set.Nontrivial.einfsep_exists_of_finite, HolderWith.edist_le, UniformOnFun.edist_eq_restrict_sUnion, ConvexBody.hausdorffEDist_coe, MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv, MeasureTheory.lintegral_norm_eq_lintegral_edist, EMetric.diam_eq_sSup, Subtype.edist_eq, ConvexBody.hausdorffEdist_coe, AntilipschitzWith.mul_le_edist, edist_pi_const, EMetric.Closeds.edist_eq, uniformity_basis_edist_nnreal, edist_triangle_left, edist_nndist, EMetric.diam_union, UniformOnFun.edist_continuousRestrict_of_singleton, dist_edist, Complex.edist_of_re_eq, edist_le_Ico_sum_edist, ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable_edist, unitInterval.volume_uIoc, edist_toDual, EMetric.cauchySeq_iff', measurable_edist, IsRiemannianManifold.out, Complex.edist_of_im_eq, UniformOnFun.edist_le, EMetric.diam_triple, HolderOnWith.edist_le_of_le, edist_vsub_vsub_le, UniformFun.edist_continuousMapMk, MeasureTheory.SimpleFunc.edist_nearestPt_le, LipschitzWith.edist_lt_top, IsCompact.exists_infEDist_eq_edist, edist_one_left, EMetric.hausdorffEdist_singleton, uniformity_basis_edist', PairReduction.iSup_edist_pairSet, ProbabilityTheory.IsAEKolmogorovProcess.aestronglyMeasurable_edist, edist_le_range_sum_of_edist_le, MeasureTheory.SimpleFunc.edist_approxOn_le, congruent_iff_edist_eq, PseudoEMetricSpace.uniformity_edist, MeasureTheory.MeasuredSets.edist_def, MeasureTheory.L1.edist_def, Set.einfsep_pos, Filter.Tendsto.edist, edist_eq_enorm_inv_mul, EuclideanSpace.edist_eq, ULift.edist_eq, MeasureTheory.Lp.edist_dist, edist_smul_le, Metric.ediam_le_iff, edist_pos, UniformSpace.Completion.edist_eq, edist_eq_enorm_neg_add, EMetric.isUniformInducing_iff, edist_eq_zero, EMetric.inseparable_iff, ContractingWith.apriori_edist_iterate_efixedPoint_le, Fin.edist_append_eq_max_edist, ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero, MeasureTheory.AEStronglyMeasurable.edist, Metric.mem_eball', PiLp.edist_eq_of_L1, edist_indicator, ContractingWith.edist_efixedPoint_le, Metric.edist_le_of_ediam_le, MeasureTheory.Integrable.edist_toL1_toL1, uniformity_pseudoedist, WithLp.prod_edist_eq_add, Metric.infEDist_lt_iff, EMetric.exists_pos_forall_lt_edist, Similar.exists_pairwise_edist_eq, uniformSpace_edist, PiLp.edist_comm, ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero, ContinuousMap.edist_eq_iSup, WithLp.edist_snd_le, eVariationOn.eq_zero_iff, Metric.mem_eball, Metric.boundedSpace_iff_edist, Metric.exists_pos_forall_lt_edist, PiLp.edist_eq_of_L2, edist_naturalParameterization_eq_zero, BoundedContinuousFunction.lintegral_le_edist_mul, Metric.ediam_insert, Set.Finite.einfsep_exists_of_nontrivial, Metric.infEDist_le_edist_add_infEDist, EMetric.edist_le_of_diam_le, TensorProduct.edist_tmul_le, edist_mulIndicator, Continuous.edist, WithLp.prod_edist_comm, PiLp.edist_single_same, PseudoEMetricSpace.edist_triangle, MeasureTheory.edist_integral_le_lintegral_edist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	edist	—	—	—
ext_iff 📖	mathematical	—	edist	—	ext

EMetric

Definitions

Name	Category	Theorems
ball 📖	CompOp	—
closedBall 📖	CompOp	—
edistLtTopSetoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball_disjoint 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring EDist.edist PseudoEMetricSpace.toEDist	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Metric.eball	—	Metric.eball_disjoint
ball_eq_empty_iff 📖	mathematical	—	Metric.eball Set Set.instEmptyCollection ENNReal instZeroENNReal	—	Metric.eball_eq_empty_iff
ball_mem_nhds 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Metric.eball	—	Metric.eball_mem_nhds
ball_prod_same 📖	mathematical	—	SProd.sprod Set Set.instSProd Metric.eball Prod.pseudoEMetricSpaceMax	—	Metric.eball_prod_same
ball_subset 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring EDist.edist PseudoEMetricSpace.toEDist	Set Set.instHasSubset Metric.eball	—	Metric.eball_subset
ball_subset_ball 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	Set Set.instHasSubset Metric.eball	—	Metric.eball_subset_eball
ball_subset_closedBall 📖	mathematical	—	Set Set.instHasSubset Metric.eball Metric.closedEBall	—	Metric.eball_subset_closedEBall
ball_zero 📖	mathematical	—	Metric.eball ENNReal instZeroENNReal Set Set.instEmptyCollection	—	Metric.eball_zero
closedBall_mem_nhds 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Metric.closedEBall	—	Metric.closedEBall_mem_nhds
closedBall_prod_same 📖	mathematical	—	SProd.sprod Set Set.instSProd Metric.closedEBall Prod.pseudoEMetricSpaceMax	—	Metric.closedEBall_prod_same
closedBall_subset_closedBall 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	Set Set.instHasSubset Metric.closedEBall	—	Metric.closedEBall_subset_closedEBall
closedBall_top 📖	mathematical	—	Metric.closedEBall Top.top ENNReal instTopENNReal Set.univ	—	Metric.closedEBall_top
closedBall_zero 📖	mathematical	—	Metric.closedEBall EMetricSpace.toPseudoEMetricSpace ENNReal instZeroENNReal Set Set.instSingletonSet	—	Metric.closedEBall_zero
dense_iff 📖	mathematical	—	Dense UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Set.Nonempty Set Set.instInter Metric.eball	—	—
exists_ball_subset_ball 📖	mathematical	Set Set.instMembership Metric.eball	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set Set.instHasSubset Metric.eball	—	Metric.exists_eball_subset_eball
instIsCountablyGeneratedUniformity 📖	mathematical	—	Filter.IsCountablyGenerated uniformity PseudoEMetricSpace.toUniformSpace	—	Filter.isCountablyGenerated_of_seq Filter.HasBasis.eq_iInf uniformity_basis_edist_inv_nat
isClosed_ball_top 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Metric.eball Top.top ENNReal instTopENNReal	—	Metric.isClosed_eball_top
isOpen_ball 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Metric.eball	—	Metric.isOpen_eball
isOpen_iff 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set Set.instHasSubset Metric.eball	—	—
mem_ball 📖	mathematical	—	Set Set.instMembership Metric.eball ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Metric.mem_eball
mem_ball' 📖	mathematical	—	Set Set.instMembership Metric.eball ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Metric.mem_eball'
mem_ball_comm 📖	mathematical	—	Set Set.instMembership Metric.eball	—	Metric.mem_eball_comm
mem_ball_self 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set Set.instMembership Metric.eball	—	Metric.mem_eball_self
mem_closedBall 📖	mathematical	—	Set Set.instMembership Metric.closedEBall ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Metric.mem_closedEBall
mem_closedBall' 📖	mathematical	—	Set Set.instMembership Metric.closedEBall ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Metric.mem_closedEBall'
mem_closedBall_comm 📖	mathematical	—	Set Set.instMembership Metric.closedEBall	—	Metric.mem_closedEBall_comm
mem_closedBall_self 📖	mathematical	—	Set Set.instMembership Metric.closedEBall	—	Metric.mem_closedEBall_self
mem_closure_iff 📖	mathematical	—	Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	mem_closure_iff_nhds_basis Metric.nhds_basis_eball PseudoEMetricSpace.edist_comm
mem_nhdsWithin_iff 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.instHasSubset Set.instInter Metric.eball	—	Filter.HasBasis.mem_iff Metric.nhdsWithin_basis_eball
mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.instHasSubset Metric.eball	—	Filter.HasBasis.mem_iff Metric.nhds_basis_eball
mk_uniformity_basis 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE	Filter.HasBasis uniformity PseudoEMetricSpace.toUniformSpace setOf ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.mem_iff uniformity_basis_edist lt_of_lt_of_le Membership.mem.out
mk_uniformity_basis_le 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE	Filter.HasBasis uniformity PseudoEMetricSpace.toUniformSpace setOf ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.mem_iff uniformity_basis_edist exists_between ENNReal.instDenselyOrdered lt_of_le_of_lt le_trans Membership.mem.out le_of_lt
nhdsWithin_basis_closed_eball 📖	mathematical	—	Filter.HasBasis ENNReal nhdsWithin UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set Set.instInter Metric.closedEBall	—	Metric.nhdsWithin_basis_closedEBall
nhdsWithin_basis_eball 📖	mathematical	—	Filter.HasBasis ENNReal nhdsWithin UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set Set.instInter Metric.eball	—	Metric.nhdsWithin_basis_eball
nhds_basis_closed_eball 📖	mathematical	—	Filter.HasBasis ENNReal nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Metric.closedEBall	—	Metric.nhds_basis_closedEBall
nhds_basis_eball 📖	mathematical	—	Filter.HasBasis ENNReal nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Metric.eball	—	Metric.nhds_basis_eball
nhds_eq 📖	mathematical	—	nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace iInf Filter ENNReal Filter.instInfSet Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Filter.principal Metric.eball	—	Filter.HasBasis.eq_biInf Metric.nhds_basis_eball
ordConnected_setOf_ball_subset 📖	mathematical	—	Set.OrdConnected ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder setOf Set Set.instHasSubset Metric.eball	—	Metric.ordConnected_setOf_eball_subset
ordConnected_setOf_closedBall_subset 📖	mathematical	—	Set.OrdConnected ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder setOf Set Set.instHasSubset Metric.closedEBall	—	Metric.ordConnected_setOf_closedEBall_subset
pos_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	—	Metric.pos_of_mem_eball
tendsto_atTop 📖	mathematical	—	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeSup.toPartialOrder nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.tendsto_iff Filter.atTop_basis SemilatticeSup.instIsDirectedOrder Metric.nhds_basis_eball
tendsto_nhds 📖	mathematical	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.tendsto_right_iff Metric.nhds_basis_eball
tendsto_nhdsWithin_nhds 📖	mathematical	—	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace nhds ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist	—	nhdsWithin_univ tendsto_nhdsWithin_nhdsWithin
tendsto_nhdsWithin_nhdsWithin 📖	mathematical	—	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set Set.instMembership EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.tendsto_iff Metric.nhdsWithin_basis_eball
tendsto_nhds_nhds 📖	mathematical	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.tendsto_iff Metric.nhds_basis_eball
uniformContinuousOn_iff 📖	mathematical	—	UniformContinuousOn PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.uniformContinuousOn_iff uniformity_basis_edist
uniformContinuous_iff 📖	mathematical	—	UniformContinuous PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.uniformContinuous_iff uniformity_basis_edist

EMetricSpace

Definitions

Name	Category	Theorems
induced 📖	CompOp	1 math math: isometry_induced
replaceTopology 📖	CompOp	—
replaceUniformity 📖	CompOp	—
toPseudoEMetricSpace 📖	CompOp	508 math math: MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory, ContinuousLinearEquiv.antilipschitz, EMetric.diam_pos_iff', LipschitzWith.max_const, MemHolder.nsmul, Unitization.isometry_inr, NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal, IsometryEquiv.dimH_preimage, LightCondensed.isoFinYonedaComponents_hom_apply, EuclideanGeometry.side_angle_side, NonUnitalIsometricContinuousFunctionalCalculus.isometric, HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn, MeasureTheory.hausdorffMeasure_segment, ConvexOn.continuousOn_tfae, ConcaveOn.locallyLipschitz, MemHolder.holderWith, IsometryEquiv.toRealLinearIsometryEquiv_symm_apply, Metric.exists_continuous_real_forall_closedEBall_subset, MemHolder.comp, ext_iff, ApproximatesLinearOn.lipschitz, ContractingWith.edist_le_of_fixedPoint, NumberField.InfinitePlace.isometry_embedding, GromovHausdorff.isometry_optimalGHInjr, MeasureTheory.UniformIntegrable.uniformIntegrable_of_tendstoInMeasure, LipschitzWith.lipschitzWith_compLp, EMetric.NonemptyCompacts.lipschitz_prod, LightCondSet.continuous_coinducingCoprod, Complex.lipschitz_equivRealProd, AntilipschitzWith.isClosed_range, IsometryEquiv.toRealLinearIsometryEquiv_apply, Metric.exists_forall_closedEBall_subset_aux₂, TopologicalSpace.Compacts.lipschitz_prod, LipschitzWith.completion_extension, ODE.FunSpace.range_toContinuousMap, Delone.DeloneSet.isCover_coveringRadius, Real.ediam_eq, EMetric.NonemptyCompacts.isometry_toCloseds, MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, lintegral_fderiv_lineMap_eq_edist, Real.volume_closedEBall, ContinuousLinearMap.isometry_mul_flip, Delone.DeloneSet.mapIsometry_trans, Set.infsep_zero_iff_subsingleton_of_finite, UpperHalfPlane.isometry_real_vadd, TopologicalSpace.Compacts.edist_eq, EMetric.Closeds.isometry_singleton, ContDiff.lipschitzWith_of_hasCompactSupport, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn, IsometryEquiv.midpoint_fixed, ContinuousMapZero.isometry_toContinuousMap, TopologicalSpace.NonemptyCompacts.isClosed_in_closeds, MeasureTheory.Measure.mkMetric_apply, HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv, AntilipschitzWith.isUniformEmbedding, ConcaveOn.locallyLipschitzOn_interior, eHolderNorm_eq_zero, Perfect.small_diam_splitting, MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum, EMetric.exists_continuous_nnreal_forall_closedBall_subset, MemHolder.coe_nnHolderNorm_eq_eHolderNorm, UpperHalfPlane.isometry_vertical_line, TopologicalSpace.NonemptyCompacts.isometry_singleton, MeasureTheory.Integrable.edist_toL1_zero, Complex.isometry_conj, Metric.t4Space, WithAbs.isometry_of_comp, ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith, Finset.infsep_pos_iff_nontrivial, HasFiniteFPowerSeriesOnBall.cpolynomialOn, UnitAddTorus.mFourierCoeff_toLp, lipschitzWith_sup_right, MeasureTheory.tendsto_integral_approxOn_of_measurable, MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo, TopologicalSpace.Compacts.lipschitz_sup, MeasureTheory.Measure.mkMetric_le_liminf_tsum, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp, HasFPowerSeriesWithinOnBall.differentiableOn, DomAddAct.instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp, Metric.ediam_pos_iff', ContinuousLinearMap.antilipschitz_of_isEmbedding, metrizableSpace, ContractingWith.apriori_edist_iterate_efixedPoint_le', hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall, NumberField.InfinitePlace.Completion.isometry_extensionEmbedding, MeasureTheory.Integrable.norm_toL1, antilipschitzWith_mul_right, Real.ediam_Ioc, LinearMap.exists_antilipschitzWith, Metric.exists_forall_closedEBall_subset_aux₁, IsometryEquiv.hausdorffMeasure_image, AntilipschitzWith.isEmbedding, ConvexOn.locallyLipschitz, LipschitzWith.dist_left, Delone.DeloneSet.mapIsometry_symm_apply_carrier, HasFPowerSeriesWithinOnBall.analyticOn, LipschitzWith.of_le_add, MeasureTheory.SimpleFunc.nnnorm_approxOn_le, lipschitzOnWith_cfc_fun_of_subset, Dilation.isClosedEmbedding, EMetric.closedBall_zero, Metric.isPreconnected_closedEBall, Real.volume_emetric_closedBall, IsLowerSet.cthickening, HasFPowerSeriesOnBall.differentiableOn, Metric.isPathConnected_closedEBall, LocallyLipschitz.const_max, MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure, Isometry.completion_map, holderWith_zero_iff, LipschitzWith.projIcc, BoundedContinuousFunction.Lp_nnnorm_le, EMetric.countable_closure_of_compact, unitInterval.volume_uIcc, Metric.toGlueL_isometry, IsCompactOperator.antilipschitz_of_not_hasEigenvalue, Dense.lipschitzWith_extend, lipschitzWith_thickenedIndicator, TopologicalSpace.NonemptyCompacts.lipschitz_prod, MeasureTheory.lintegral_edist_triangle, unitInterval.volume_uIoo, Set.Finite.infsep_pos_iff_nontrivial, MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset, MonotoneOn.locallyBoundedVariationOn, MeasureTheory.lintegral_edist_lt_top, BoundedVariationOn.sub_le, IsPicardLindelof.lipschitzOnWith, MeasureTheory.hasFiniteIntegral_iff_edist, EMetric.exists_forall_closedBall_subset_aux₂, ContractingWith.edist_efixedPoint_lt_top', HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt, isometry_cfcₙHom, HasStrictFDerivAt.exists_lipschitzOnWith, Complex.antilipschitz_equivRealProd, Complex.isometry_ofReal, lipschitzWith_one_norm', LocallyLipschitz.max, MeasureTheory.SimpleFunc.norm_approxOn_y₀_le, ContractingWith.edist_efixedPoint_le', MeasureTheory.SimpleFunc.memLp_approxOn_range, Metric.eventually_nhds_zero_forall_closedEBall_subset, DilationEquiv.mulRight_symm_apply, algebraMap_isometry, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, IsUpperSet.thickening', TopologicalSpace.Closeds.lipschitz_sup, Metric.coveringNumber_zero, DilationEquiv.mulLeft_symm_apply, IsometryEquiv.map_midpoint, Dilation.isUniformEmbedding, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, NNReal.lipschitzWith_sub, LightCondensed.isoFinYonedaComponents_inv_comp, EuclideanSpace.edist_single_same, lipschitzWith_circleMap, HasFPowerSeriesWithinOnBall.continuousOn, MeasureTheory.Lp.mem_boundedContinuousFunction_iff, LipschitzWith.min, DilationEquiv.mulLeft_apply, Real.lipschitzWith_sin, TopologicalSpace.Closeds.edist_eq, Set.infsep_pos_iff_nontrivial_of_finite, MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm, TopologicalSpace.Closeds.isometry_singleton, lipschitzOnWith_cfc_fun, Isometry.isometryEquivOnRange_toEquiv, MeasureTheory.hausdorffMeasure_prod_real, MemHolder.add, AffineMap.lipschitzWith_of_finiteDimensional, ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective, AntilipschitzWith.isClosedEmbedding, Convex.lipschitzOnWith_of_nnnorm_fderiv_le, LipschitzWith.min_const, ContinuousLinearMap.antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range, LightCondensed.isoLocallyConstantOfIsColimit_inv, Real.volume_pi_le_prod_diam, WithLp.volume_preserving_toLp, LipschitzOnWith.extend_real, UniformSpace.Completion.coe_isometry, LipschitzWith.coordinate, HasFiniteFPowerSeriesOnBall.differentiableOn, TopologicalSpace.Compacts.isometry_singleton, LipschitzOnWith.extend_finite_dimension, Delone.DeloneSet.mapIsometry_symm, Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, LipschitzOnWith.extend_lp_infty, Metric.isPreconnected_eball, IsometryEquiv.map_hausdorffMeasure, MeasureTheory.Lp.lipschitzWith_pos_part, PiNat.exists_lipschitz_retraction_of_isClosed, fourierCoeff_toLp, Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn', Isometry.completion_extension, MemHolder.smul, LipschitzWith.const_min, Metric.ediam_pos_iff, ContinuousLinearMap.isometry_iff_adjoint_comp_self, GromovHausdorff.ghDist_eq_hausdorffDist, ContinuousLinearMap.opNorm_extend_le, Metric.exists_continuous_nnreal_forall_closedEBall_subset, ApproximatesLinearOn.lipschitz_sub, lp.lipschitzWith_one_eval, HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal, Set.relatively_discrete_of_finite, Isometry.isEmbedding, Emetric.exists_contMDiffMap_forall_closedBall_subset, ContractingWith.tendsto_iterate_efixedPoint, DilationEquiv.mulRight_apply, nhds_eq_nhds_emetric_ball, lipschitzOnWith_cfcₙ_fun, LocallyLipschitz.min_const, Delone.DeloneSet.mapIsometry_refl, BoundedContinuousFunction.mem_Lp, EMetric.exists_forall_closedBall_subset_aux₁, BoundedContinuousFunction.Lp_norm_le, IsometryEquiv.hausdorffMeasure_preimage, TopologicalSpace.Closeds.continuous_infEDist, KuratowskiEmbedding.embeddingOfSubset_isometry, EMetric.isUniformEmbedding_iff', ContractingWith.exists_fixedPoint, RCLike.lipschitzWith_re, instIsRiemannianManifoldModelWithCornersSelfReal, TopologicalSpace.NonemptyCompacts.isometry_toCloseds, BoundedVariationOn.stieltjesFunctionRightLim_apply, Isometry.isometryEquivOnRange_apply, UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal, ApproximatesLinearOn.antilipschitz, Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt, IsometryEquiv.measurePreserving_hausdorffMeasure, IsUpperSet.thickening, EMetric.subsingleton_iff_indiscreteTopology, isometry_induced, TopologicalSpace.Closeds.instCompleteSpace, EuclideanGeometry.similar_of_side_angle_side, Metric.isSeparated_zero, GromovHausdorff.AuxGluingStruct.isom, TopologicalSpace.Closeds.lipschitz_prod, Real.lipschitzWith_one_mulExpNegMulSq, ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range, HasFiniteFPowerSeriesOnBall.continuousOn, MeasureTheory.SimpleFunc.memLp_approxOn, memHolder_iff_holderWith, IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero, ContractingWith.toLipschitzWith, ContDiff.locallyLipschitz, HasFTaylorSeriesUpToOn.exists_lipschitzOnWith, Isometry.coveringNumber_image, MeasureTheory.MeasuredSets.lipschitzWith_measureReal, MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum, eHolderNorm_nsmul, LipschitzWith.dist_right, ConvexOn.locallyLipschitzOn_iff_continuousOn, Metric.closedEBall_zero, HasFPowerSeriesOnBall.analyticOnNhd, Set.Finite.infsep_zero_iff_subsingleton, variationOnFromTo.sub_self_monotoneOn, IsometryEquiv.dimH_image, Metric.exists_continuous_ennreal_forall_closedEBall_subset, EMetric.NonemptyCompacts.isClosed_in_closeds, EMetric.exists_continuous_real_forall_closedBall_subset, ContractingWith.edist_inequality, Set.Finite.relatively_discrete, Real.volume_eball, LipschitzWith.completion_map, Real.volume_le_diam, MeasureTheory.L1.dist_def, NumberField.InfinitePlace.isometry_embedding_of_isReal, edist_le_zero, FormalMultilinearSeries.analyticOnNhd, LipschitzOnWith.extend_pi, ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt, uniformity_edist, LipschitzOnWith.coordinate, LipschitzOnWith.iff_le_add_mul, Metric.isCompact_closure_iff_exists_finite_isCover, AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp, EMetric.diam_pos_iff, lipschitzWith_negPart, MeasureTheory.OuterMeasure.isometryEquiv_map_mkMetric, ContinuousMap.coe_toLp, Real.lipschitzWith_toNNReal, DomMulAct.instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp, antilipschitz_of_bound_of_norm_one, MeasureTheory.SimpleFunc.integrable_approxOn_range, Set.einfsep_pos_of_finite, ConvexOn.locallyLipschitzOn_interior, LipschitzWith.of_le_add_mul, Delone.DeloneSet.mapBilipschitz_trans, lipschitzWith_of_nnnorm_fderiv_le, MemHolder.nnHolderNorm_nsmul, LipschitzWith.max, lipschitzWith_one_nnnorm, WithLp.volume_preserving_symm_measurableEquiv_toLp_prod, eventually_riemannianEDist_le_edist_extChartAt, EuclideanGeometry.similar_of_angle_angle, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz, lipschitzOnWith_cfcₙ_fun_of_subset, ProbabilityTheory.condExp_ae_eq_integral_condDistrib', EMetric.nontrivial_iff_nontrivialTopology, ContractingWith.exists_fixedPoint', HasFPowerSeriesOnBall.unique, AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp, Metric.isometry_inl, LocallyLipschitz.max_const, LipschitzWith.iff_le_add_mul, ContractingWith.edist_efixedPoint_lt_top, EuclideanGeometry.triangle_congruent_iff_dist_eq, MemHolder.nnHolderNorm_smul, Metric.toInductiveLimit_isometry, Convex.lipschitz_gauge, MeasureTheory.tendstoInMeasure_of_tendsto_Lp, antilipschitzWith_mul_left, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real, Real.ediam_Ioo, LipschitzOnWith.zero_iff, MemHolder.nnHolderNorm_add_le, Dilation.ratio_comp, Isometry.isometry_mapRingHom, MeasureTheory.SimpleFunc.integrable_approxOn, ConvexOn.locallyLipschitzOn, Metric.toGlueR_isometry, Isometry.isClosedEmbedding, Submodule.lipschitzWith_starProjection, Real.volume_pi_le_diam_pow, Finset.infsep_zero_iff_subsingleton, LipschitzOnWith.of_le_add, TopologicalSpace.NonemptyCompacts.lipschitz_sup, Metric.contractibleSpace_eball, ConcaveOn.locallyLipschitzOn, WithLp.volume_preserving_ofLp, Metric.isConnected_closedEBall, GromovHausdorff.toGHSpace_lipschitz, NonUnitalStarAlgHom.isometry, Isometry.isUniformEmbedding, IsometryEquiv.coeFn_toRealAffineIsometryEquiv, IsLowerSet.thickening, ContDiffOn.exists_lipschitzOnWith, eHolderNorm_add_le, MeasureTheory.dist_integral_le_lintegral_edist, Convex.lipschitzWith_gauge, ConcaveOn.exists_lipschitzOnWith_of_isBounded, MeasureTheory.lintegral_enorm_eq_lintegral_edist, HasFPowerSeriesWithinOnBall.unique, MeasureTheory.SimpleFunc.norm_approxOn_zero_le, EuclideanGeometry.angle_side_angle, MeasureTheory.Measure.hausdorffMeasure_apply, RCLike.lipschitzWith_ofReal, LocallyLipschitz.const_min, zero_eq_edist, ConvexOn.exists_lipschitzOnWith_of_isBounded, Metric.lipschitz_infDist_pt, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, instT0Space, EuclideanGeometry.angle_angle_side, Submodule.lipschitzWith_orthogonalProjection, EuclideanGeometry.side_side_side, lipschitzWith_of_nnnorm_deriv_le, Real.lipschitzWith_cos, MeasureTheory.Measure.mkMetric_le_liminf_sum, Metric.ediam_eq_zero_iff, Metric.lipschitz_infDist, NormedSpace.continuousOn_exp, EMetric.Closeds.lipschitz_sup, MeasureTheory.hausdorffMeasure_affineSegment, EMetric.NonemptyCompacts.isometry_singleton, Metric.eball_contractible, IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero_symm, HolderWith.nnholderNorm_le, MonotoneOn.eVariationOn_le, MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz, ContractingWith.eq_or_edist_eq_top_of_fixedPoints, Metric.isPathConnected_eball, Dilation.mulRight_toFun, MeasureTheory.BoundedContinuousFunction.inner_toLp, tendsto_measure_cthickening_of_isCompact, Metric.contractibleSpace_closedEBall, NNReal.isometry_coe, HasFPowerSeriesOnBall.continuousOn, EMetric.instNontrivialTopologyOfNontrivial, ConcaveOn.continuousOn_tfae, lp.isometry_single, Delone.DeloneSet.isSeparated_packingRadius, LipschitzOnWith.of_le_add_mul', Set.Finite.einfsep_pos, Metric.lipschitz_infDist_set, Metric.packingNumber_zero, Unitization.antilipschitzWith_addEquiv, Emetric.exists_smooth_forall_closedBall_subset, Metric.Sigma.isometry_mk, IsUpperSet.cthickening', MeasureTheory.lintegral_norm_eq_lintegral_edist, Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt, MeasureTheory.tendsto_setToFun_approxOn_of_measurable, MemHolder.nnHolderNorm_eq_zero, gelfandTransform_isometry, EMetric.exists_continuous_eNNReal_forall_closedBall_subset, MeasureTheory.isometry_lpMeasSubgroupToLpTrim, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, EMetric.Closeds.edist_eq, ContractingWith.tendsto_iterate_efixedPoint', LinearMap.antilipschitz_of_comap_nhds_le, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith, bsupr_limsup_dimH, IsLowerSet.thickening', lipschitzWith_one_nnnorm', KuratowskiEmbedding.exists_isometric_embedding, Metric.isConnected_eball, Complex.edist_of_re_eq, EMetric.t4Space, Complex.exists_cthickening_tendstoUniformlyOn, unitInterval.volume_uIoc, lipschitzWith_max, Metric.isometry_inr, EMetric.eventually_nhds_zero_forall_closedBall_subset, lipschitzWith_lineMap, Dilation.mulLeft_toFun, MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm, Unitization.lipschitzWith_addEquiv, Complex.edist_of_im_eq, EMetric.diam_eq_zero_iff, IsometricContinuousFunctionalCalculus.isometric, Metric.PiNatEmbed.isUniformEmbedding_embed, Dilation.isEmbedding, MeasureTheory.ContinuousMap.inner_toLp, lipschitzWith_posPart, HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn', NumberField.InfinitePlace.LiesOver.isometry_algebraMap, MetricSpace.isometry_induced, Metric.isCover_zero, MeasureTheory.tendsto_integral_norm_approxOn_sub, IsometryEquiv.measurePreserving_euclideanHausdorffMeasure, AffineMap.antilipschitzWith_of_finiteDimensional, AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp, MeasureTheory.L1.edist_def, antilipschitzWith_lineMap, LinearMap.injective_iff_antilipschitz, UpperHalfPlane.isometry_pos_mul, ContDiffOn.locallyLipschitzOn, eHolderNorm_smul, ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz, EuclideanSpace.edist_eq, ApproximatesLinearOn.lipschitzOnWith, edist_pos, LipschitzWith.const_max, UniformSpace.Completion.edist_eq, FormalMultilinearSeries.continuousOn, edist_eq_zero, EMetric.NonemptyCompacts.lipschitz_sup, ContractingWith.apriori_edist_iterate_efixedPoint_le, ContDiffAt.exists_lipschitzOnWith, ContDiffWithinAt.exists_lipschitzOnWith, TopologicalSpace.Compacts.isometry_toCloseds, lipschitzWith_min, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite, TopologicalSpace.NonemptyCompacts.isometry_toCompacts, ContractingWith.edist_efixedPoint_le, AffineSubspace.euclideanHausdorffMeasure_coe_image, IsLowerSet.cthickening', Convex.lipschitzOnWith_of_nnnorm_deriv_le, GromovHausdorff.isometry_optimalGHInjl, AbsoluteValue.Completion.extensionEmbedding_of_comp_coe, Metric.lipschitz_infNndist_pt, MeasureTheory.Integrable.edist_toL1_toL1, WithLp.unitization_isometry_inr, MeasureTheory.L1.setToL1_lipschitz, GromovHausdorff.eq_toGHSpace_iff, LipschitzOnWith.of_le_add_mul, LipschitzWith.zero_iff, MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm, Metric.externalCoveringNumber_zero, IsUniformEmbedding.to_isometry, MeasureTheory.Lp.isometry_compMeasurePreserving, iSup_limsup_dimH, MemHolder.smul_iff, ODE.FunSpace.lipschitzWith, ConcaveOn.locallyLipschitzOn_iff_continuousOn, LocallyLipschitz.min, Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le, LipschitzWith.of_le_add_mul', RCLike.lipschitzWith_im, EMetric.continuous_infEdist_hausdorffEdist, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm, BoundedContinuousFunction.lintegral_le_edist_mul, Real.ediam_Icc, IsUpperSet.cthickening, ConvexOn.lipschitzOnWith_of_abs_le, HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt, Metric.exists_contMDiffMap_forall_closedEBall_subset, StarAlgEquiv.isometry, Delone.DeloneSet.mapIsometry_apply_carrier, TopologicalSpace.NonemptyCompacts.instSecondCountableTopology, Convex.lipschitzOnWith_of_nnnorm_derivWithin_le, Complex.isometry_intCast, kuratowskiEmbedding.isometry, Real.ediam_Ico, ContinuousLinearMap.antilipschitz_of_forall_le_inner_map, TensorProduct.edist_tmul_le, LipschitzWith.dist, isometry_cfcHom, Real.volume_emetric_ball, MeasureTheory.OuterMeasure.isometryEquiv_comap_mkMetric, lipschitzWith_one_norm, ConcaveOn.lipschitzOnWith_of_abs_le, IsCoercive.antilipschitz, MeasureTheory.edist_integral_le_lintegral_edist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_edist_eq_zero 📖	—	EDist.edist PseudoEMetricSpace.toEDist toPseudoEMetricSpace ENNReal instZeroENNReal	—	—	—
ext 📖	—	PseudoEMetricSpace.toEDist toPseudoEMetricSpace	—	—	PseudoEMetricSpace.ext
ext_iff 📖	mathematical	—	PseudoEMetricSpace.toEDist toPseudoEMetricSpace	—	ext

Metric

Definitions

Name	Category	Theorems
closedEBall 📖	CompOp	100 math math: closedEBall_mem_nhds, IsometryEquiv.image_emetric_closedBall, Dilation.mapsTo_closedEBall, exists_continuous_real_forall_closedEBall_subset, EMetric.nhdsWithin_basis_closed_eball, mem_closedEBall, exists_forall_closedEBall_subset_aux₂, ediam_closedEBall_le, Real.volume_closedEBall, emetric_closedBall, Isometry.preimage_closedEBall, IsometryEquiv.preimage_emetric_closedBall, EMetric.preimage_mul_right_closedBall, preimage_mul_right_closedEBall, EMetric.exists_continuous_nnreal_forall_closedBall_subset, smul_closedEBall, EMetric.mem_closedBall, closedEBall_ofReal, Snowflaking.image_toSnowflaking_emetricClosedBall, IsometryEquiv.image_closedEBall, EMetric.closedBall_mem_nhds, Isometry.mapsTo_closedEBall, EMetric.preimage_mul_left_closedBall, preimage_smul_closedEBall, exists_forall_closedEBall_subset_aux₁, Snowflaking.preimage_toSnowflaking_emetricClosedBall, EMetric.closedBall_zero, isPreconnected_closedEBall, Real.volume_emetric_closedBall, isPathConnected_closedEBall, eball_subset_closedEBall, preimage_vadd_closedEBall, EMetric.exists_forall_closedBall_subset_aux₂, Subtype.preimage_closedEBall, mem_closedEBall_self, Isometry.mapsTo_emetric_closedBall, IsometryEquiv.preimage_closedEBall, preimage_add_left_closedEBall, Dilation.mapsTo_emetric_closedBall, disjoint_closedEBall_of_lt_infEDist, Snowflaking.image_ofSnowflaking_closedEBall, mem_closedEBall', EMetric.ordConnected_setOf_closedBall_subset, Subtype.image_emetricClosedBall, ordConnected_setOf_closedEBall_subset, exists_continuous_nnreal_forall_closedEBall_subset, preimage_mul_left_closedEBall, Emetric.exists_contMDiffMap_forall_closedBall_subset, EMetric.exists_forall_closedBall_subset_aux₁, EMetric.mem_closedBall_self, convex_closedEBall, EMetric.ball_subset_closedBall, EMetric.closedBall_subset_closedBall, measure_closedEBall_pos, Snowflaking.preimage_toSnowflaking_closedEBall, nhdsWithin_basis_closedEBall, closedEBall_zero, vadd_closedEBall, exists_continuous_ennreal_forall_closedEBall_subset, EMetric.exists_continuous_real_forall_closedBall_subset, EMetric.mem_closedBall_comm, EMetric.vadd_closedBall, EMetric.closedBall_top, emetric_closedBall_nnreal, EMetric.mem_closedBall', mem_closedEBall_comm, EMetric.nhds_basis_closed_eball, EMetric.preimage_smul_closedBall, preimage_add_right_closedEBall, isConnected_closedEBall, Snowflaking.image_ofSnowflaking_emetricClosedBall, EMetric.disjoint_closedBall_of_lt_infEdist, Snowflaking.image_toSnowflaking_closedEBall, closedEBall_top, isCover_iff_subset_iUnion_closedEBall, LipschitzWith.mapsTo_emetric_closedBall, contractibleSpace_closedEBall, nhds_basis_closedEBall, Emetric.exists_smooth_forall_closedBall_subset, closedEBall_subset_closedEBall, EMetric.exists_continuous_eNNReal_forall_closedBall_subset, closedEBall_prod_same, Snowflaking.preimage_ofSnowflaking_emetricClosedBall, EMetric.isClosed_closedBall, EMetric.closedBall_prod_same, isCover_iff_subset_iUnion_emetricClosedBall, closedEBall_coe, EMetric.smul_closedBall, EMetric.preimage_add_left_closedBall, EMetric.measure_closedBall_pos, Snowflaking.preimage_ofSnowflaking_closedEBall, Isometry.preimage_emetric_closedBall, Subtype.preimage_emetricClosedBall, isClosed_closedEBall, Subtype.image_closedEBall, LipschitzWith.mapsTo_closedEBall, EMetric.diam_closedBall, exists_contMDiffMap_forall_closedEBall_subset, EMetric.preimage_add_right_closedBall, EMetric.preimage_vadd_closedBall
eball 📖	CompOp	137 math math: nhdsWithin_basis_eball, isOpen_eball, HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn, Dilation.mapsTo_eball, EMetric.mem_ball_self, eball_subset_eball, eball_top_eq_univ, lebesgue_number_lemma_of_emetric_nhds, EMetric.isOpen_iff, EMetric.dense_iff, EMetric.ball_prod_same, EMetric.smul_ball, eball_ofReal, EMetric.ball_disjoint, EMetric.vadd_ball, emetric_ball, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn, HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, IsCompact.uniform_oscillation, IsometryEquiv.image_emetric_ball, EMetric.mem_ball, Subtype.image_emetricBall, EMetric.isClosed_ball_top, EMetric.exists_ball_subset_ball, Isometry.mapsTo_eball, HasFiniteFPowerSeriesOnBall.cpolynomialOn, EMetric.nhdsWithin_basis_eball, HasFPowerSeriesWithinOnBall.differentiableOn, hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall, mem_eball_comm, HasFPowerSeriesWithinOnBall.analyticOn, EMetric.mem_ball_comm, Snowflaking.image_ofSnowflaking_eball, eball_subset, IsometryEquiv.preimage_emetric_ball, Snowflaking.image_toSnowflaking_eball, HasFPowerSeriesOnBall.differentiableOn, IsometryEquiv.image_eball, eball_subset_closedEBall, emetric_ball_top, EMetric.preimage_mul_left_ball, EMetric.diam_ball, eball_zero, EMetric.nhds_basis_eball, Isometry.mapsTo_emetric_ball, convex_eball, lebesgue_number_lemma_of_emetric_sUnion, preimage_smul_eball, HasFPowerSeriesWithinOnBall.continuousOn, EMetric.preimage_add_right_ball, preimage_mul_right_eball, emetric_ball_nnreal, mem_emetric_ball_one_iff, lebesgue_number_lemma_of_emetric_nhdsWithin', HasFiniteFPowerSeriesOnBall.differentiableOn, isPreconnected_eball, ediam_eball_le, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn', exists_eball_subset_eball, EMetric.ball_zero, EMetric.ball_subset, HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal, EMetric.mem_ball', nhds_eq_nhds_emetric_ball, eball_top, Snowflaking.preimage_toSnowflaking_eball, eball_prod_same, mem_eball_one_iff, EMetric.ball_subset_closedBall, HasFiniteFPowerSeriesOnBall.continuousOn, eball_mem_nhds, EMetric.preimage_mul_right_ball, HasFPowerSeriesOnBall.analyticOnNhd, Real.volume_eball, FormalMultilinearSeries.analyticOnNhd, lebesgue_number_lemma_of_emetric, LipschitzWith.mapsTo_emetric_ball, smul_eball, EMetric.mem_nhds_iff, lebesgue_number_lemma_of_emetric_nhdsWithin, EMetric.measure_ball_pos, isClosed_eball_top, HasFPowerSeriesOnBall.unique, preimage_mul_left_eball, measure_eball_pos, ordConnected_setOf_eball_subset, nhds_basis_eball, Subtype.preimage_eball, Subtype.image_eball, LipschitzWith.mapsTo_eball, eball_disjoint, EMetric.totallyBounded_iff, measurableSet_eball, contractibleSpace_eball, Subtype.preimage_emetricBall, EMetric.nhds_eq, HasFPowerSeriesWithinOnBall.unique, Snowflaking.preimage_ofSnowflaking_eball, EMetric.preimage_add_left_ball, NormedSpace.continuousOn_exp, eball_contractible, isPathConnected_eball, EMetric.ball_subset_ball, EMetric.ordConnected_setOf_ball_subset, HasFPowerSeriesOnBall.continuousOn, eball_eq_empty_iff, mem_emetric_ball_zero_iff, preimage_add_right_eball, Snowflaking.preimage_ofSnowflaking_emetricBall, vadd_eball, Dilation.mapsTo_emetric_ball, eball_coe, mem_eball_self, isConnected_eball, EMetric.preimage_smul_ball, EMetric.isOpen_ball, mem_eball_zero_iff, HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn', lebesgue_number_lemma_of_emetric_nhds', preimage_vadd_eball, Snowflaking.image_ofSnowflaking_emetricBall, Isometry.preimage_eball, preimage_add_left_eball, EMetric.mem_nhdsWithin_iff, IsCompact.uniform_oscillationWithin, EMetric.totallyBounded_iff', FormalMultilinearSeries.continuousOn, mem_eball', Snowflaking.preimage_toSnowflaking_emetricBall, Isometry.preimage_emetric_ball, EMetric.ball_mem_nhds, EMetric.ball_eq_empty_iff, Snowflaking.image_toSnowflaking_emetricBall, EMetric.preimage_vadd_ball, mem_eball, IsometryEquiv.preimage_eball, Real.volume_emetric_ball
edistLtTopSetoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedEBall_mem_nhds 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace closedEBall	—	Filter.mem_of_superset eball_mem_nhds eball_subset_closedEBall
closedEBall_prod_same 📖	mathematical	—	SProd.sprod Set Set.instSProd closedEBall Prod.pseudoEMetricSpaceMax	—	Set.ext
closedEBall_subset_closedEBall 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	Set Set.instHasSubset closedEBall	—	le_trans
closedEBall_top 📖	mathematical	—	closedEBall Top.top ENNReal instTopENNReal Set.univ	—	Set.eq_univ_of_forall Set.mem_setOf le_top
closedEBall_zero 📖	mathematical	—	closedEBall EMetricSpace.toPseudoEMetricSpace ENNReal instZeroENNReal Set Set.instSingletonSet	—	Set.ext ENNReal.instCanonicallyOrderedAdd
eball_disjoint 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring EDist.edist PseudoEMetricSpace.toEDist	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice eball	—	Set.disjoint_left LE.le.not_gt edist_triangle_left LT.lt.trans_le ENNReal.add_lt_add
eball_eq_empty_iff 📖	mathematical	—	eball Set Set.instEmptyCollection ENNReal instZeroENNReal	—	Set.eq_empty_iff_forall_notMem le_bot_iff le_of_not_gt mem_eball_self not_lt_of_ge le_of_eq pos_of_mem_eball
eball_mem_nhds 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace eball	—	IsOpen.mem_nhds isOpen_eball mem_eball_self
eball_prod_same 📖	mathematical	—	SProd.sprod Set Set.instSProd eball Prod.pseudoEMetricSpaceMax	—	Set.ext
eball_subset 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring EDist.edist PseudoEMetricSpace.toEDist	Set Set.instHasSubset eball	—	PseudoEMetricSpace.edist_triangle add_comm ENNReal.add_lt_add_left
eball_subset_closedEBall 📖	mathematical	—	Set Set.instHasSubset eball closedEBall	—	le_of_lt Membership.mem.out
eball_subset_eball 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	Set Set.instHasSubset eball	—	lt_of_lt_of_le
eball_zero 📖	mathematical	—	eball ENNReal instZeroENNReal Set Set.instEmptyCollection	—	eball_eq_empty_iff
exists_eball_subset_eball 📖	mathematical	Set Set.instMembership eball	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set Set.instHasSubset eball	—	ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub eball_subset Eq.le add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid LT.lt.le mem_eball ne_top_of_lt
isClosed_eball_top 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace eball Top.top ENNReal instTopENNReal	—	isOpen_compl_iff EMetric.isOpen_iff ENNReal.coe_lt_top
isOpen_eball 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace eball	—	EMetric.isOpen_iff exists_eball_subset_eball
mem_closedEBall 📖	mathematical	—	Set Set.instMembership closedEBall ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	—
mem_closedEBall' 📖	mathematical	—	Set Set.instMembership closedEBall ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	PseudoEMetricSpace.edist_comm mem_closedEBall
mem_closedEBall_comm 📖	mathematical	—	Set Set.instMembership closedEBall	—	mem_closedEBall' mem_closedEBall
mem_closedEBall_self 📖	mathematical	—	Set Set.instMembership closedEBall	—	mem_closedEBall PseudoEMetricSpace.edist_self zero_le ENNReal.instCanonicallyOrderedAdd
mem_eball 📖	mathematical	—	Set Set.instMembership eball ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	—
mem_eball' 📖	mathematical	—	Set Set.instMembership eball ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	PseudoEMetricSpace.edist_comm mem_eball
mem_eball_comm 📖	mathematical	—	Set Set.instMembership eball	—	mem_eball' mem_eball
mem_eball_self 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set Set.instMembership eball	—	mem_eball PseudoEMetricSpace.edist_self
nhdsWithin_basis_closedEBall 📖	mathematical	—	Filter.HasBasis ENNReal nhdsWithin UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set Set.instInter closedEBall	—	nhdsWithin_hasBasis nhds_basis_closedEBall
nhdsWithin_basis_eball 📖	mathematical	—	Filter.HasBasis ENNReal nhdsWithin UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set Set.instInter eball	—	nhdsWithin_hasBasis nhds_basis_eball
nhds_basis_closedEBall 📖	mathematical	—	Filter.HasBasis ENNReal nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal closedEBall	—	nhds_basis_uniformity uniformity_basis_edist_le
nhds_basis_eball 📖	mathematical	—	Filter.HasBasis ENNReal nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal eball	—	nhds_basis_uniformity uniformity_basis_edist
ordConnected_setOf_closedEBall_subset 📖	mathematical	—	Set.OrdConnected ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder setOf Set Set.instHasSubset closedEBall	—	HasSubset.Subset.trans Set.instIsTransSubset closedEBall_subset_closedEBall
ordConnected_setOf_eball_subset 📖	mathematical	—	Set.OrdConnected ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder setOf Set Set.instHasSubset eball	—	HasSubset.Subset.trans Set.instIsTransSubset eball_subset_eball
pos_of_mem_eball 📖	mathematical	Set Set.instMembership eball	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	—	lt_of_le_of_lt zero_le ENNReal.instCanonicallyOrderedAdd

MulOpposite

Definitions

Name	Category	Theorems
instPseudoEMetricSpace 📖	CompOp	4 math math: edist_op, isometry_opLinearEquiv, edist_unop, instIsIsometricSMulMulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_op 📖	mathematical	—	EDist.edist MulOpposite PseudoEMetricSpace.toEDist instPseudoEMetricSpace op	—	—
edist_unop 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist unop MulOpposite instPseudoEMetricSpace	—	—

Prod

Definitions

Name	Category	Theorems
pseudoEMetricSpaceMax 📖	CompOp	68 math math: edist_eq, LipschitzWith.prodMk_right, LocallyLipschitz.prodMk, IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph, LipschitzWith.prod_snd, EMetric.NonemptyCompacts.lipschitz_prod, Complex.lipschitz_equivRealProd, TopologicalSpace.Compacts.lipschitz_prod, EMetric.ball_prod_same, lipschitzWith_lipschitz_const_add_edist, isIsometricVAdd'', HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, Fin.appendIsometry_symm_apply, TopologicalSpace.Compacts.lipschitz_sup, LipschitzWith.prod_fst, TopologicalSpace.NonemptyCompacts.lipschitz_prod, Fin.appendIsometryOfEq_apply, LipschitzOnWith.prodMk, WithLp.prod_isometry_ofLp_infty, Complex.antilipschitz_equivRealProd, lipschitzWith_lipschitz_const_mul_edist, instIsIsometricSMul, TopologicalSpace.Closeds.lipschitz_sup, NNReal.lipschitzWith_sub, LipschitzWith.prodMk, WithLp.prod_antilipschitzWith_toLp, LipschitzMul.lipschitz_mul, WithLp.prod_lipschitzWith_ofLp, HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal, LipschitzWith.uncurry, IsometryEquiv.piFinTwo_symm_apply, isIsometricSMul'', Fin.appendIsometry_toHomeomorph, WithLp.prod_lipschitzWith_toLp, IsometryEquiv.sumArrowIsometryEquivProdArrow_symm_apply, Metric.eball_prod_same, TopologicalSpace.Closeds.lipschitz_prod, Isometry.prodMap, LocallyLipschitz.prodMk_left, Isometry.inl, Metric.infEDist_prod, Metric.hausdorffEDist_prod_le, LipschitzWith.prodMk_left, Fin.appendIsometryOfEq_symm_apply, SeminormedAddCommGroup.lipschitzWith_sub, TopologicalSpace.NonemptyCompacts.lipschitz_sup, EMetric.hausdorffEdist_prod_le, EMetric.infEdist_prod, Metric.lipschitz_infDist, Isometry.inr, EMetric.Closeds.lipschitz_sup, IsometryEquiv.piFinTwo_apply, Unitization.antilipschitzWith_addEquiv, Fin.appendIsometry_apply, Metric.closedEBall_prod_same, isIsometricSMul', EMetric.closedBall_prod_same, lipschitzWith_max, Unitization.lipschitzWith_addEquiv, instIsIsometricVAdd, IsometryEquiv.sumArrowIsometryEquivProdArrow_apply, EMetric.NonemptyCompacts.lipschitz_sup, lipschitzWith_min, LipschitzAdd.lipschitz_add, LipschitzWith.dist, WithLp.prod_antilipschitzWith_ofLp, LocallyLipschitz.prodMk_right, isIsometricVAdd'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_eq 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist pseudoEMetricSpaceMax ENNReal ENNReal.instMax	—	—

PseudoEMetricSpace

Definitions

Name	Category	Theorems
induced 📖	CompOp	1 math math: isometry_induced
ofEDistOfTopology 📖	CompOp	—
replaceUniformity 📖	CompOp	—
toEDist 📖	CompOp	375 math math: MeasureTheory.tendstoInMeasure_iff_measureReal_norm, edist_eq_enorm_sub, edist_congr_left, Prod.edist_eq, eVariationOn.sum_le_of_monotoneOn_Icc, edist_comm, MeasureTheory.hausdorffMeasure_segment, WithLp.edist_fst_le, Metric.isSeparated_insert_of_notMem, PiLp.edist_self, LipschitzWith.edist_lt_of_edist_lt_div, EMetricSpace.ext_iff, edist_le_of_edist_le_geometric_two_of_tendsto₀, EMetric.le_infEdist, MeasureTheory.MeasuredSets.sub_le_edist, ContractingWith.edist_le_of_fixedPoint, edist_mem_uniformity, MeasureTheory.TendstoInMeasure.exists_seq_tendstoInMeasure_atTop, edist_div_right, UniformFun.edist_eval_le, Congruent.pairwise_edist_eq, HolderWith.edist_le_of_le, MeasureTheory.UniformIntegrable.uniformIntegrable_of_tendstoInMeasure, Metric.mem_closedEBall, Set.le_einfsep_of_forall_dist_le, MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable, Set.einfsep_lt_top_iff, uniformity_basis_edist, edist_zero_left, edist_le_Ico_sum_of_edist_le, MeasureTheory.LevyProkhorov.edist_measure_def, lintegral_fderiv_lineMap_eq_edist, edist_zero_eq_enorm, Metric.isSeparated_iff_setRelIsSeparated, AffineIsometryEquiv.edist_map, Set.infsep_zero_iff_subsingleton_of_finite, Metric.infEDist_le_edist_of_mem, Isometry.edist_eq, TopologicalSpace.Compacts.edist_eq, MeasureTheory.SimpleFunc.nearestPtInd_succ, EMetric.diam_pair, DilationEquiv.edist_eq', EMetric.diam_le_iff, Metric.ediam_triple, edist_le_of_edist_le_geometric_of_tendsto, Metric.PiNatEmbed.edist_def, MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top, measurable_edist_right, EMetric.mem_ball, MeasureTheory.Integrable.edist_toL1_zero, Metric.infEDist_le_infEDist_add_edist, EMetric.mem_closedBall, congruent_iff_pairwise_edist_eq, EMetric.exists_edist_lt_of_hausdorffEdist_lt, Finset.infsep_pos_iff_nontrivial, uniformity_basis_edist_le, EMetric.isUniformEmbedding_iff, MulOpposite.edist_op, DilationClass.edist_eq', edist_div_left, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp, AddOpposite.edist_op, edist_le_of_edist_le_geometric_two_of_tendsto, Set.Finite.infsep_of_nontrivial, MeasureTheory.tendstoInMeasure_iff_norm, MeasureTheory.StronglyMeasurable.edist, EMetric.diam_insert, ContractingWith.apriori_edist_iterate_efixedPoint_le', PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius, EMetric.uniformContinuous_iff, MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_measurable_edist, IsometryEquiv.edist_eq, MeasureTheory.Integrable.norm_toL1, MeasureTheory.TendstoInMeasure.indicator, edist_le_tsum_of_edist_le_of_tendsto₀, LinearIsometry.edist_map, Finset.coe_infsep_of_offDiag_nonempty, Set.Nontrivial.infsep_of_fintype, Set.infsep_le_of_mem_of_edist_le, MeasureTheory.tendstoInMeasure_iff_measureReal_dist, Set.Finite.infsep, edist_le_tsum_of_edist_le_of_tendsto, edist_neg, EMetric.cauchySeq_iff, PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius, EMetric.tendsto_nhds, uniformity_basis_edist_le', WithLp.edist_toLp_snd, Dilation.edist_eq', EMetric.mk_uniformity_basis_le, similar_iff_exists_edist_eq, MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure, Set.Nontrivial.infsep_eq_iInf, Metric.isSeparated_insert, unitInterval.volume_uIcc, MeasureTheory.lintegral_edist_triangle, MeasureTheory.tendstoInMeasure_iff_dist, variationOnFromTo.eq_zero_iff_of_le, unitInterval.volume_uIoo, Set.Finite.infsep_pos_iff_nontrivial, WithLp.prod_edist_eq_of_L2, MulOpposite.edist_unop, EMetric.infEdist_singleton, eVariationOn.sum_le_of_monotoneOn_Iic, UniformOnFun.edist_eval_le, MeasureTheory.lintegral_edist_lt_top, Dilation.edist_eq, MeasureTheory.LevyProkhorov.edist_finiteMeasure_def, MeasureTheory.hasFiniteIntegral_iff_edist, ContractingWith.edist_efixedPoint_lt_top', edist_mul_mul_le, edist_mul_right, continuous_edist, EMetric.controlled_of_isUniformEmbedding, PairReduction.edist_le_of_mem_pairSet, edist_sub_left, Set.infsep_eq_iInf, AddOpposite.edist_unop, MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_spec, Metric.ediam_eq_sSup, ContractingWith.edist_efixedPoint_le', AEMeasurable.edist, Set.infsep_pair, MeasureTheory.SimpleFunc.edist_approxOn_y0_le, Set.einfsep_eq_top_iff, LipschitzWith.edist_iterate_succ_le_geometric, SeparationQuotient.edist_mk, Set.einfsep_insert, uniformity_basis_edist_inv_nat, MeasureTheory.SimpleFunc.edist_approxOn_mono, EuclideanSpace.edist_single_same, ProbabilityTheory.IsKolmogorovProcess.measurable_edist, Set.Nontrivial.infsep_lt_iff, Metric.mem_closedEBall', TopologicalSpace.Closeds.edist_eq, LipschitzWith.edist_le_mul, ProbabilityTheory.IsAEKolmogorovProcess.kolmogorovCondition, Set.infsep_pos_iff_nontrivial_of_finite, MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm, ProbabilityTheory.IsKolmogorovProcess.kolmogorovCondition, EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt, Set.infsep_of_fintype, LipschitzOnWith.edist_lt_of_edist_lt_div, LipschitzOnWith.edist_le_mul_of_le, Metric.le_infEDist, edist_neg_neg, edist_vadd_left, ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero, edist_one_right, EMetric.tendsto_nhds_nhds, Metric.edist_le_ediam_of_mem, Set.Finite.infsep_exists_of_nontrivial, UniformFun.edist_le, edist_self, edist_triangle4, edist_triangle_right, ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist, ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero_of_const_eq_zero, LipschitzWith.mul_edist_le, Metric.edist_le_infEDist_add_ediam, EMetric.mem_ball', LipschitzWith.edist_le_mul_of_le, Set.relatively_discrete_of_finite, EMetric.infEdist_le_edist_add_infEdist, Finset.coe_infsep, edist_one_eq_enorm, edist_smul₀, uniformity_basis_edist_nnreal_le, Inseparable.edist_eq_zero, edist_eq_enorm_div, EMetric.isUniformEmbedding_iff', EMetric.pair_reduction, ContractingWith.exists_fixedPoint, variationOnFromTo.eq_zero_iff_of_ge, uniformity_basis_edist_inv_two_pow, EMetric.tendsto_atTop, EMetric.edist_le_infEdist_add_ediam, edist_add_add_le, similar_iff_exists_pairwise_edist_eq, PiLp.edist_apply_le, edist_sub_right, AntilipschitzWith.edist_lt_top, eVariationOn.edist_le, Metric.mem_thickening_iff_exists_edist_lt, UniformOnFun.edist_def', EMetric.edist_le_diam_of_mem, LinearIsometryEquiv.edist_map, Set.Nontrivial.infsep_anti, EMetric.cauchySeq_iff_le_tendsto_0, Set.Finite.infsep_zero_iff_subsingleton, Finset.coe_infsep_of_offDiag_empty, MeasureTheory.LevyProkhorov.edist_probabilityMeasure_def, ContractingWith.edist_inequality, Set.Finite.relatively_discrete, measurable_edist_left, Metric.ediam_pair, MeasureTheory.tendstoInMeasure_iff_measureReal_enorm, MeasureTheory.L1.dist_def, Set.Nontrivial.infsep_exists_of_finite, UniformFun.edist_def, edist_le_zero, uniformity_edist, hasConstantSpeedOnWith_zero_iff, EMetric.infEdist_le_edist_of_mem, edist_add_left, eVariationOn.sum_le, Set.infsep_triple, eVariationOn.add_point, Set.einfsep_pos_of_finite, edist_smul_left, WithLp.prod_edist_eq_of_L1, EMetric.diam_image_le_iff, Congruent.edist_eq, Set.infsep_le_dist_of_mem, UniformOnFun.edist_def, eventually_riemannianEDist_le_edist_extChartAt, variationOnFromTo.edist_zero_of_eq_zero, eVariationOn.eVariationOn_eq_strictMonoOn, Similar.exists_edist_eq, Metric.infEDist_singleton, WithLp.prod_edist_self, DilationEquivClass.edist_eq', LipschitzWith.edist_lt_mul_of_lt, ContractingWith.exists_fixedPoint', BoundedContinuousFunction.edist_eq_iSup, ContractingWith.edist_efixedPoint_lt_top, MeasureTheory.tendstoInMeasure_of_tendsto_Lp, edist_congr, EMetric.mem_closedBall', edist_mul_left, Metric.ediam_image_le_iff, EMetric.tendsto_nhdsWithin_nhds, Finset.infsep_zero_iff_subsingleton, edist_congr_right, UniformOnFun.edist_continuousRestrict, EMetric.cauchy_iff, EMetric.uniformContinuousOn_iff, edist_le_range_sum_edist, MeasureTheory.Egorov.mem_notConvergentSeq_iff, PiLp.edist_toLp_single_same, Set.infsep_pair_eq_toReal, edist_add_right, EMetric.mk_uniformity_basis, edist_vadd_vadd_le, Metric.exists_edist_lt_of_hausdorffEDist_lt, PairReduction.exists_radius_le, Set.einfsep_triple, EMetric.mem_closure_iff, IsometryClass.edist_eq, EMetric.infEdist_lt_iff, Set.Nontrivial.le_infsep, MeasureTheory.dist_integral_le_lintegral_edist, edist_zero_right, Subtype.edist_mk_mk, MeasureTheory.lintegral_enorm_eq_lintegral_edist, tendsto_iff_edist_tendsto_0, EMetric.infEdist_le_infEdist_add_edist, MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top, edist_le_of_edist_le_geometric_of_tendsto₀, Measurable.edist, edist_inv_inv, Metric.hausdorffEDist_singleton, zero_eq_edist, MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff, Set.einfsep_pair, EMetric.cauchySeq_iff_NNReal, Metric.ediam_union_le_add_edist, variationOnFromTo.eq_zero_iff, edist_pi_const_le, MeasureTheory.hausdorffMeasure_affineSegment, IsCompact.exists_infEdist_eq_edist, AffineIsometry.edist_map, ULift.edist_up_up, ContractingWith.eq_or_edist_eq_top_of_fixedPoints, Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt, HolderOnWith.edist_le, EMetric.tendsto_nhdsWithin_nhdsWithin, edist_inv, Set.Finite.einfsep_pos, WithLp.edist_toLp_fst, MeasureTheory.tendstoInMeasure_iff_enorm, HolderWith.edist_le, ConvexBody.hausdorffEDist_coe, MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv, MeasureTheory.lintegral_norm_eq_lintegral_edist, EMetric.diam_eq_sSup, Subtype.edist_eq, ConvexBody.hausdorffEdist_coe, AntilipschitzWith.mul_le_edist, Set.Nontrivial.einfsep_lt_top, edist_pi_const, EMetric.Closeds.edist_eq, uniformity_basis_edist_nnreal, edist_triangle_left, EMetric.diam_union, UniformOnFun.edist_continuousRestrict_of_singleton, Complex.edist_of_re_eq, edist_le_Ico_sum_edist, ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable_edist, unitInterval.volume_uIoc, EMetric.cauchySeq_iff', measurable_edist, IsRiemannianManifold.out, Complex.edist_of_im_eq, UniformOnFun.edist_le, EMetric.diam_triple, HolderOnWith.edist_le_of_le, edist_vsub_vsub_le, UniformFun.edist_continuousMapMk, MeasureTheory.SimpleFunc.edist_nearestPt_le, LipschitzWith.edist_lt_top, IsCompact.exists_infEDist_eq_edist, edist_one_left, MeasureTheory.tendstoInMeasure_of_tendsto_ae, EMetric.hausdorffEdist_singleton, uniformity_basis_edist', PairReduction.iSup_edist_pairSet, ProbabilityTheory.IsAEKolmogorovProcess.aestronglyMeasurable_edist, edist_le_range_sum_of_edist_le, MeasureTheory.SimpleFunc.edist_approxOn_le, congruent_iff_edist_eq, uniformity_edist, MeasureTheory.MeasuredSets.edist_def, MeasureTheory.L1.edist_def, Filter.Tendsto.edist, edist_eq_enorm_inv_mul, EuclideanSpace.edist_eq, ULift.edist_eq, edist_smul_le, Metric.ediam_le_iff, edist_pos, UniformSpace.Completion.edist_eq, edist_eq_enorm_neg_add, EMetric.isUniformInducing_iff, edist_eq_zero, EMetric.inseparable_iff, ContractingWith.apriori_edist_iterate_efixedPoint_le, Fin.edist_append_eq_max_edist, ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite, MeasureTheory.AEStronglyMeasurable.edist, Metric.mem_eball', PiLp.edist_eq_of_L1, edist_indicator, ContractingWith.edist_efixedPoint_le, Metric.edist_le_of_ediam_le, MeasureTheory.Integrable.edist_toL1_toL1, uniformity_pseudoedist, Metric.infEDist_lt_iff, EMetric.exists_pos_forall_lt_edist, Similar.exists_pairwise_edist_eq, Set.Nontrivial.le_infsep_iff, uniformSpace_edist, PiLp.edist_comm, ext_iff, ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero, ContinuousMap.edist_eq_iSup, WithLp.edist_snd_le, eVariationOn.eq_zero_iff, Metric.mem_eball, Metric.exists_pos_forall_lt_edist, PiLp.edist_eq_of_L2, edist_naturalParameterization_eq_zero, BoundedContinuousFunction.lintegral_le_edist_mul, Metric.ediam_insert, Metric.infEDist_le_edist_add_infEDist, Set.le_einfsep_pi_of_le, EMetric.edist_le_of_diam_le, TensorProduct.edist_tmul_le, edist_mulIndicator, Continuous.edist, WithLp.prod_edist_comm, PiLp.edist_single_same, edist_triangle, MeasureTheory.edist_integral_le_lintegral_edist
toUniformSpace 📖	CompOp	372 math math: BoundedVariationOn.continuousWithinAt_leftLim, Metric.nhdsWithin_basis_eball, Matrix.l2_opNorm_toEuclideanCLM, MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory, MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed, Metric.closedEBall_mem_nhds, Metric.cthickening_closure, Metric.isOpen_eball, Dilation.tendsto_nhds_iff, thickenedIndicator_mono_infEDist, IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph, Metric.exists_continuous_real_forall_closedEBall_subset, MeasureTheory.Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq, Matrix.cstar_nnnorm_def, DilationEquiv.coe_toHomeomorph, Metric.hausdorffEDist_closure, edist_mem_uniformity, thickenedIndicatorAux_tendsto_indicator_closure, Isometry.uniformContinuous, thickenedIndicator_one_of_mem_closure, EMetric.nhdsWithin_basis_closed_eball, EMetric.isOpen_iff, EMetric.NonemptyCompacts.lipschitz_prod, LipschitzOnWith.uniformEquicontinuousOn, EMetric.dense_iff, AntilipschitzWith.isClosed_range, TopologicalSpace.Compacts.lipschitz_prod, HasStrictFDerivAt.rightFun_implicitFunctionDataOfProdDomain, uniformity_basis_edist, EMetric.NonemptyCompacts.isometry_toCloseds, isClosed_setOf_lipschitzOnWith, cauchySeq_of_edist_le_of_tsum_ne_top, TopologicalSpace.Compacts.edist_eq, IsCompact.exists_thickening_image_subset, EMetric.Closeds.isometry_singleton, TopologicalSpace.NonemptyCompacts.isClosed_in_closeds, IsometryEquiv.coe_toHomeomorph, isClosed_setOf_tendsto_birkhoffAverage, EMetric.infEdist_pos_iff_notMem_closure, BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici, Isometry.comp_continuous_iff, AntilipschitzWith.isUniformEmbedding, EMetric.exists_continuous_nnreal_forall_closedBall_subset, EMetric.tendstoLocallyUniformlyOn_iff, indicator_thickening_eventually_eq_indicator_closure, lipschitzOnWith_closure_iff, eVariationOn.eVariationOn_rightLim_le, Metric.hausdorffEDist_closure_right, TopologicalSpace.NonemptyCompacts.isometry_singleton, Metric.hausdorffEDist_self_closure, continuous_prod_of_continuous_lipschitzWith, Metric.t4Space, LipschitzOnWith.closure, LipschitzOnWith.continuousOn, EMetric.isClosed_ball_top, DilationEquiv.coe_symm_toHomeomorph, EMetric.closedBall_mem_nhds, uniformity_basis_edist_le, thickenedIndicator_zero, EMetric.isUniformEmbedding_iff, MeasureTheory.tendsto_integral_approxOn_of_measurable, MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo, TopologicalSpace.Compacts.lipschitz_sup, Metric.isOpen_thickening, EMetric.nhdsWithin_basis_eball, Metric.ediam_closure, thickenedIndicator_le_one, HasMFDerivWithinAt.prodMap, MeasureTheory.integrable_thickenedIndicator, EMetricSpace.metrizableSpace, thickenedIndicatorAux_closure_eq, EMetric.mem_closure_iff_infEdist_zero, EMetric.uniformContinuous_iff, BoundedVariationOn.exists_tendsto_atTop, Metric.exists_forall_closedEBall_subset_aux₁, AntilipschitzWith.isEmbedding, BoundedVariationOn.exists_tendsto_left_of_filter, EMetric.tendstoUniformly_iff, Module.Basis.prod_addHaar, cauchySeq_of_edist_le_of_summable, Dilation.isClosedEmbedding, EMetric.cauchySeq_iff, IsometryEquiv.comp_continuousOn_iff, EMetric.infEdist_closure_pos_iff_notMem_closure, EMetric.tendsto_nhds, uniformity_basis_edist_le', IsOpen.exists_iUnion_isClosed, EMetric.mk_uniformity_basis_le, AntilipschitzWith.isInducing, HasFPowerSeriesWithinOnBall.prod, IsometryEquiv.completeSpace, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith', cauchySeq_of_edist_le_geometric_two, Matrix.toEuclideanCLM_toLp, EMetric.countable_closure_of_compact, IsIsometricSMul.to_continuousConstSMul, Dense.lipschitzWith_extend, lipschitzWith_thickenedIndicator, TopologicalSpace.NonemptyCompacts.lipschitz_prod, continuous_of_le_add_edist, MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset, Dilation.toContinuous, Bundle.Trivialization.continuousLinearEquivAt_prod, tendsto_measure_cthickening, Metric.frontier_thickening_subset, continuous_edist, BoundedVariationOn.leftLim, AntilipschitzWith.isUniformInducing, dist_integral_mulExpNegMulSq_comp_le, Metric.cthickening_zero, MeasureTheory.SimpleFunc.memLp_approxOn_range, Metric.eventually_nhds_zero_forall_closedEBall_subset, Isometry.tendsto_nhds_iff, EMetric.nhds_basis_eball, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, TopologicalSpace.Closeds.lipschitz_sup, IsometryEquiv.completeSpace_iff, Dilation.isUniformEmbedding, SeparationQuotient.edist_mk, uniformity_basis_edist_inv_nat, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, pseudoMetrizableSpace, continuousOn_prod_of_continuousOn_lipschitzOnWith, indicator_le_thickenedIndicator, TopologicalSpace.Closeds.edist_eq, Metric.closure_eq_iInter_cthickening, Oscillation.eq_zero_iff_continuousAt, TopologicalSpace.Closeds.isometry_singleton, BoundedVariationOn.tendsto_leftLim, BoundedVariationOn.tendsto_atTop_limUnder, Matrix.inner_toEuclideanCLM, tendsto_measure_thickening, MeasureTheory.hausdorffMeasure_prod_real, DilationEquiv.toHomeomorph_symm, AntilipschitzWith.isClosedEmbedding, EMetric.diam_closure, WithLp.volume_preserving_toLp, EMetric.tendsto_nhds_nhds, Metric.mem_closure_iff_infEDist_zero, TopologicalSpace.Compacts.isometry_singleton, IsIsometricVAdd.to_continuousConstVAdd, Matrix.ofLp_toEuclideanCLM, measure_le_lintegral_thickenedIndicator, EMetric.instIsCountablyGeneratedUniformity, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, one_le_thickenedIndicator_apply', LocallyLipschitzOn.continuousOn, EMetric.subset_countable_closure_of_almost_dense_set, Metric.exists_continuous_nnreal_forall_closedEBall_subset, MeasureTheory.SimpleFunc.tendsto_approxOn, Isometry.isEmbedding, Metric.closure_thickening_subset_cthickening, Metric.infEDist_closure_pos_iff_notMem_closure, Emetric.exists_contMDiffMap_forall_closedBall_subset, ContractingWith.tendsto_iterate_efixedPoint, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto', nhds_eq_nhds_emetric_ball, Dilation.isUniformInducing, HasStrictFDerivAt.leftFun_implicitFunctionDataOfProdDomain, Metric.thickening_subset_interior_cthickening, MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero, EMetric.exists_forall_closedBall_subset_aux₁, Fin.appendIsometry_toHomeomorph, thickenedIndicator_tendsto_indicator_closure, uniformity_basis_edist_nnreal_le, TopologicalSpace.Closeds.continuous_infEDist, EMetric.isUniformEmbedding_iff', LipschitzWith.uniformContinuous, Dilation.comp_continuousOn_iff, Metric.hasBasis_nhdsSet_cthickening, ContractingWith.exists_fixedPoint, TopologicalSpace.NonemptyCompacts.isometry_toCloseds, uniformity_basis_edist_inv_two_pow, EMetric.tendstoLocallyUniformly_iff, EMetric.tendsto_atTop, EMetric.subsingleton_iff_indiscreteTopology, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, TopologicalSpace.Closeds.instCompleteSpace, Isometry.continuous, LipschitzWith.uniformEquicontinuous, TopologicalSpace.Closeds.lipschitz_prod, HolderWith.uniformContinuous, MeasureTheory.SimpleFunc.memLp_approxOn, EMetric.secondCountable_of_sigmaCompact, Metric.hausdorffEDist_zero_iff_closure_eq_closure, Metric.cthickening_mem_nhdsSet, Metric.closure_subset_cthickening, Metric.eball_mem_nhds, LipschitzWith.continuous, EMetric.cauchySeq_iff_le_tendsto_0, EMetric.infEdist_closure, BoundedVariationOn.exists_tendsto_left, IsClopen.of_cthickening_subset_self, HasFPowerSeriesWithinAt.prod, Metric.nhdsWithin_basis_closedEBall, ProbabilityTheory.IsKolmogorovProcess.measurablePair, Metric.exists_continuous_ennreal_forall_closedEBall_subset, EMetric.NonemptyCompacts.isClosed_in_closeds, EMetric.exists_continuous_real_forall_closedBall_subset, HolderOnWith.uniformContinuousOn, cauchySeq_of_edist_le_geometric, thickenedIndicator_subset, Dilation.comp_continuous_iff, uniformity_edist, HasFTaylorSeriesUpToOn.prodMk, LocallyLipschitz.continuous, Metric.frontier_thickening_disjoint, thickenedIndicator_apply, BoundedVariationOn.exists_tendsto_right, Metric.hausdorffEDist_closure_left, WithLp.isUniformInducing_toLp, indicator_cthickening_eventually_eq_indicator_closure, MeasureTheory.SimpleFunc.integrable_approxOn_range, IsometryEquiv.comp_continuous_iff', EMetric.mem_nhds_iff, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist', Isometry.comp_continuousOn_iff, EMetric.hausdorffEdist_zero_iff_closure_eq_closure, WithLp.volume_preserving_symm_measurableEquiv_toLp_prod, MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed, Metric.isClosed_eball_top, BoundedVariationOn.rightLim, EMetric.nontrivial_iff_nontrivialTopology, PiLp.isUniformInducing_toLp, ContractingWith.exists_fixedPoint', Metric.hasBasis_nhdsSet_thickening, continuous_prod_of_dense_continuous_lipschitzWith', thickenedIndicator_mono_infEdist, continuousOn_prod_of_continuousOn_lipschitzOnWith', IsClopen.of_thickening_subset_self, MeasureTheory.SimpleFunc.tendsto_nearestPt, Metric.nhds_basis_eball, eVariationOn.lowerSemicontinuous_uniformOn, Metric.closure_eq_iInter_thickening', MeasureTheory.SimpleFunc.integrable_approxOn, measurableSet_of_continuousAt, Metric.frontier_cthickening_disjoint, Isometry.isClosedEmbedding, EMetric.tendsto_nhdsWithin_nhds, EMetric.nhds_basis_closed_eball, EMetric.cauchy_iff, EMetric.uniformContinuousOn_iff, HasFPowerSeriesOnBall.prod, Metric.instParacompactSpace, MeasureTheory.MeasuredSets.continuous_measure, EMetric.mk_uniformity_basis, TopologicalSpace.NonemptyCompacts.lipschitz_sup, EMetric.totallyBounded_iff, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist, tendsto_mulIndicator_thickening_mulIndicator_closure, EMetric.complete_of_convergent_controlled_sequences, uniformEquicontinuous_birkhoffAverage, Metric.infEDist_closure, WithLp.volume_preserving_ofLp, Isometry.isUniformEmbedding, EMetric.mem_closure_iff, tendsto_indicator_cthickening_indicator_closure, EMetric.nhds_eq, continuous_prod_of_dense_continuous_lipschitzWith, tendsto_iff_edist_tendsto_0, EMetric.secondCountable_of_almost_dense_set, Metric.continuous_infEDist, Metric.isClosed_cthickening, MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, EMetricSpace.instT0Space, EMetric.cauchySeq_iff_NNReal, Metric.closure_eq_iInter_cthickening', EMetric.tendstoUniformlyOn_iff, EMetric.Closeds.lipschitz_sup, EMetric.NonemptyCompacts.isometry_singleton, HasFPowerSeriesAt.prod, AntilipschitzWith.comap_nhds_le, EMetric.tendsto_nhdsWithin_nhdsWithin, EMetric.instNontrivialTopologyOfNontrivial, AntilipschitzWith.isComplete_range, continuous_thickenedIndicatorAux, Metric.nhds_basis_closedEBall, Metric.cthickening_of_nonpos, Isometry.isUniformInducing, IsometryClass.toContinuousMapClass, thickenedIndicator_one, EMetric.hausdorffEdist_closure, uniformity_eq_of_bilipschitz, Emetric.exists_smooth_forall_closedBall_subset, IsometryClass.continuous, MeasureTheory.tendsto_setToFun_approxOn_of_measurable, IsometryClass.toHomeomorphClass, HolderWith.continuous, EMetric.exists_continuous_eNNReal_forall_closedBall_subset, IsometryEquiv.toEquiv_toHomeomorph, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, EMetric.isClosed_closedBall, EMetric.Closeds.edist_eq, ContractingWith.tendsto_iterate_efixedPoint', uniformity_basis_edist_nnreal, Metric.frontier_cthickening_subset, EMetric.complete_of_cauchySeq_tendsto, Metric.thickening_mem_nhdsSet, bsupr_limsup_dimH, mulIndicator_cthickening_eventually_eq_mulIndicator_closure, Bundle.Prod.contMDiffVectorBundle, EMetric.t4Space, UniformOnFun.continuous_of_forall_lipschitzWith, Matrix.cstar_norm_def, BoundedVariationOn.exists_tendsto_atBot, EMetric.cauchySeq_iff', HasStrictFDerivAt.pt_implicitFunctionDataOfProdDomain, EMetric.eventually_nhds_zero_forall_closedBall_subset, EMetric.isOpen_ball, Metric.closure_subset_thickening, MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto, mulIndicator_thickening_eventually_eq_mulIndicator_closure, IsCompact.exists_isCompact_cthickening, Metric.PiNatEmbed.isUniformEmbedding_embed, Dilation.isEmbedding, EMetric.hausdorffEdist_self_closure, uniformity_basis_edist', MeasureTheory.tendsto_integral_norm_approxOn_sub, IsometryEquiv.continuous, uniformity_edist, tendsto_mulIndicator_cthickening_mulIndicator_closure, BoundedVariationOn.tendsto_atBot_limUnder, EMetric.subset_countable_closure_of_compact, EMetric.hausdorffEdist_closure₂, EMetric.mem_nhdsWithin_iff, EMetric.continuous_infEdist, BoundedVariationOn.tendsto_rightLim, EMetric.totallyBounded_iff', continuous_prod_of_continuous_lipschitzWith', one_le_thickenedIndicator_apply, eVariationOn.lowerSemicontinuous, EMetric.isUniformInducing_iff, EMetric.NonemptyCompacts.lipschitz_sup, isClosed_setOf_lipschitzWith, EMetric.inseparable_iff, TopologicalSpace.Compacts.isometry_toCloseds, HolderOnWith.continuousOn, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp, TopologicalSpace.NonemptyCompacts.isometry_toCompacts, eVariationOn.eVariationOn_leftLim_le, AffineSubspace.euclideanHausdorffMeasure_coe_image, tendsto_indicator_thickening_indicator_closure, uniformity_pseudoedist, VectorBundle.prod, uniformSpace_edist, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae', EMetric.ball_mem_nhds, IsometryEquiv.coe_toHomeomorph_symm, OscillationWithin.eq_zero_iff_continuousWithinAt, BoundedVariationOn.continuousWithinAt_rightLim, mem_uniformity_edist, iSup_limsup_dimH, Metric.isClosed_closedEBall, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith, EMetric.continuous_infEdist_hausdorffEdist, EMetric.hausdorffEdist_closure₁, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm, RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict, Metric.closure_eq_iInter_thickening, Metric.exists_contMDiffMap_forall_closedEBall_subset, thickenedIndicator.coeFn_eq_comp, TopologicalSpace.NonemptyCompacts.instSecondCountableTopology, HasStrictFDerivAt.implicitFunctionOfProdDomain_def, Metric.thickening_closure, IsometryEquiv.comp_continuous_iff, Metric.infEDist_pos_iff_notMem_closure, thickenedIndicator_mono, MeasureTheory.TendstoInMeasure.aestronglyMeasurable, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto, LipschitzOnWith.uniformContinuousOn, AntilipschitzWith.comap_uniformity_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_comm 📖	mathematical	—	EDist.edist toEDist	—	—
edist_self 📖	mathematical	—	EDist.edist toEDist ENNReal instZeroENNReal	—	—
edist_triangle 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist toEDist Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	—
ext 📖	—	toEDist	—	—	UniformSpace.ext
ext_iff 📖	mathematical	—	toEDist	—	ext
uniformity_edist 📖	mathematical	—	uniformity toUniformSpace iInf Filter ENNReal Filter.instInfSet Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Filter.principal setOf EDist.edist toEDist	—	—

PseudoEmetricSpace

Definitions

Name	Category	Theorems
ofEdistOfTopology 📖	CompOp	—

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_eq 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist instPseudoEMetricSpaceSubtype	—	—
edist_mk_mk 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist instPseudoEMetricSpaceSubtype	—	—
image_closedEBall 📖	mathematical	—	Set.image Metric.closedEBall instPseudoEMetricSpaceSubtype Set Set.instInter setOf	—	preimage_closedEBall Set.image_preimage_eq_inter_range range_val_subtype
image_eball 📖	mathematical	—	Set.image Metric.eball instPseudoEMetricSpaceSubtype Set Set.instInter setOf	—	preimage_eball Set.image_preimage_eq_inter_range range_val_subtype
image_emetricBall 📖	mathematical	—	Set.image Metric.eball instPseudoEMetricSpaceSubtype Set Set.instInter setOf	—	image_eball
image_emetricClosedBall 📖	mathematical	—	Set.image Metric.closedEBall instPseudoEMetricSpaceSubtype Set Set.instInter setOf	—	image_closedEBall
preimage_closedEBall 📖	mathematical	—	Set.preimage Metric.closedEBall instPseudoEMetricSpaceSubtype	—	—
preimage_eball 📖	mathematical	—	Set.preimage Metric.eball instPseudoEMetricSpaceSubtype	—	—
preimage_emetricBall 📖	mathematical	—	Set.preimage Metric.eball instPseudoEMetricSpaceSubtype	—	preimage_eball
preimage_emetricClosedBall 📖	mathematical	—	Set.preimage Metric.closedEBall instPseudoEMetricSpaceSubtype	—	preimage_closedEBall

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_eq 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist instPseudoEMetricSpaceULift	—	—
edist_up_up 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist instPseudoEMetricSpaceULift	—	—

(root)

Definitions

Name	Category	Theorems
EDist 📖	CompData	—
EMetricSpace 📖	CompData	—
PseudoEMetricSpace 📖	CompData	—
instEDistAdditive 📖	CompOp	2 math math: edist_toMul, edist_ofMul
instEDistMultiplicative 📖	CompOp	2 math math: edist_toAdd, edist_ofAdd
instEDistOrderDual 📖	CompOp	2 math math: edist_ofDual, edist_toDual
instEMetricSpaceAddOpposite 📖	CompOp	—
instEMetricSpaceAdditive 📖	CompOp	—
instEMetricSpaceMulOpposite 📖	CompOp	—
instEMetricSpaceMultiplicative 📖	CompOp	—
instEMetricSpaceOrderDual 📖	CompOp	—
instEMetricSpaceSubtype 📖	CompOp	4 math math: ContractingWith.restrict, dimH_orthogonalProjection_le, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, AffineSubspace.euclideanHausdorffMeasure_coe_image
instEMetricSpaceULift 📖	CompOp	—
instPseudoEMetricSpaceAdditive 📖	CompOp	2 math math: Additive.isIsIsometricVAdd', Additive.isIsIsometricVAdd''
instPseudoEMetricSpaceMultiplicative 📖	CompOp	2 math math: Multiplicative.isIsIsometricVAdd'', Multiplicative.isIsometricSMul'
instPseudoEMetricSpaceOrderDual 📖	CompOp	—
instPseudoEMetricSpaceSubtype 📖	CompOp	43 math math: LipschitzOnWith.mapsToRestrict, ApproximatesLinearOn.lipschitz, ODE.FunSpace.range_toContinuousMap, AntilipschitzWith.to_rightInvOn, Subtype.image_emetricBall, lipschitzOnWith_iff_restrict, HolderOnWith.holderWith, LipschitzWith.projIcc, unitInterval.volume_uIcc, unitInterval.volume_uIoo, Subtype.preimage_closedEBall, LocallyLipschitzOn.restrict, Isometry.isometryEquivOnRange_toEquiv, Subtype.image_emetricClosedBall, ApproximatesLinearOn.lipschitz_sub, EMetric.pair_reduction, Isometry.isometryEquivOnRange_apply, ApproximatesLinearOn.antilipschitz, AntilipschitzWith.to_rightInvOn', AntilipschitzWith.subtype_coe, LipschitzWith.subtype_mk, LipschitzWith.restrict, HolderWith.restrict_iff, Subtype.preimage_eball, Subtype.image_eball, Set.MapsTo.lipschitzOnWith_iff_restrict, Subtype.preimage_emetricBall, Subtype.edist_mk_mk, AntilipschitzWith.restrict, Submodule.lipschitzWith_orthogonalProjection, LipschitzOnWith.to_restrict, lipschitzOnWith_restrict, Subtype.edist_eq, isometry_subtype_coe, MeasureTheory.isometry_lpMeasSubgroupToLpTrim, unitInterval.volume_uIoc, AntilipschitzWith.codRestrict, PairReduction.iSup_edist_pairSet, LipschitzWith.subtype_val, ODE.FunSpace.lipschitzWith, Subtype.preimage_emetricClosedBall, Subtype.image_closedEBall, locallyLipschitzOn_iff_restrict
instPseudoEMetricSpaceULift 📖	CompOp	4 math math: ULift.isIsometricSMul', ULift.edist_up_up, ULift.isIsometricVAdd', ULift.edist_eq
uniformSpaceOfEDist 📖	CompOp	1 math math: uniformSpace_edist
uniformSpaceOfEDistOfHasBasis 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_congr 📖	mathematical	EDist.edist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	EDist.edist PseudoEMetricSpace.toEDist	—	edist_congr_right edist_congr_left
edist_congr_left 📖	mathematical	EDist.edist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	EDist.edist PseudoEMetricSpace.toEDist	—	PseudoEMetricSpace.edist_comm edist_congr_right
edist_congr_right 📖	mathematical	EDist.edist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	EDist.edist PseudoEMetricSpace.toEDist	—	le_antisymm zero_add PseudoEMetricSpace.edist_triangle PseudoEMetricSpace.edist_comm
edist_eq_zero 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace ENNReal instZeroENNReal	—	EMetricSpace.eq_of_edist_eq_zero PseudoEMetricSpace.edist_self
edist_le_zero 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace instZeroENNReal	—	nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd edist_eq_zero
edist_mem_uniformity 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set Filter Filter.instMembership uniformity PseudoEMetricSpace.toUniformSpace setOf ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	mem_uniformity_edist
edist_ofAdd 📖	mathematical	—	EDist.edist Multiplicative instEDistMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	—
edist_ofDual 📖	mathematical	—	EDist.edist DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual instEDistOrderDual	—	—
edist_ofMul 📖	mathematical	—	EDist.edist Additive instEDistAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	—
edist_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	ENNReal.instCanonicallyOrderedAdd
edist_toAdd 📖	mathematical	—	EDist.edist DFunLike.coe Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd instEDistMultiplicative	—	—
edist_toDual 📖	mathematical	—	EDist.edist OrderDual instEDistOrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	—
edist_toMul 📖	mathematical	—	EDist.edist DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.toMul instEDistAdditive	—	—
edist_triangle4 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	le_imp_le_of_le_of_le PseudoEMetricSpace.edist_triangle le_refl add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid
edist_triangle_left 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	PseudoEMetricSpace.edist_comm PseudoEMetricSpace.edist_triangle
edist_triangle_right 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	PseudoEMetricSpace.edist_comm PseudoEMetricSpace.edist_triangle
eq_of_forall_edist_le 📖	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	—	EMetricSpace.eq_of_edist_eq_zero eq_of_le_of_forall_lt_imp_le_of_dense ENNReal.instDenselyOrdered bot_le
mem_uniformity_edist 📖	mathematical	—	Set Filter Filter.instMembership uniformity PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.instMembership	—	Filter.HasBasis.mem_uniformity_iff uniformity_basis_edist
uniformSpace_edist 📖	mathematical	—	PseudoEMetricSpace.toUniformSpace uniformSpaceOfEDist EDist.edist PseudoEMetricSpace.toEDist PseudoEMetricSpace.edist_self PseudoEMetricSpace.edist_comm PseudoEMetricSpace.edist_triangle	—	UniformSpace.ext PseudoEMetricSpace.edist_self PseudoEMetricSpace.edist_comm PseudoEMetricSpace.edist_triangle uniformity_pseudoedist
uniformity_basis_edist 📖	mathematical	—	Filter.HasBasis ENNReal uniformity PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal setOf EDist.edist PseudoEMetricSpace.toEDist	—	PseudoEMetricSpace.edist_self PseudoEMetricSpace.edist_comm PseudoEMetricSpace.edist_triangle UniformSpace.hasBasis_ofFun one_pos IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero uniformSpace_edist
uniformity_basis_edist' 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Filter.HasBasis ENNReal uniformity PseudoEMetricSpace.toUniformSpace Set Set.instMembership Set.Ioo PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal setOf Preorder.toLT EDist.edist PseudoEMetricSpace.toEDist	—	EMetric.mk_uniformity_basis exists_between ENNReal.instDenselyOrdered lt_min lt_of_le_of_lt min_le_right min_le_left
uniformity_basis_edist_inv_nat 📖	mathematical	—	Filter.HasBasis uniformity PseudoEMetricSpace.toUniformSpace setOf ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	EMetric.mk_uniformity_basis ENNReal.inv_pos ENNReal.natCast_ne_top ENNReal.exists_inv_nat_lt ne_of_gt le_of_lt
uniformity_basis_edist_inv_two_pow 📖	mathematical	—	Filter.HasBasis uniformity PseudoEMetricSpace.toUniformSpace setOf ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	—	EMetric.mk_uniformity_basis Nat.instAtLeastTwoHAddOfNat ENNReal.pow_pos ENNReal.inv_pos ENNReal.ofNat_ne_top ENNReal.exists_inv_two_pow_lt ne_of_gt le_of_lt
uniformity_basis_edist_le 📖	mathematical	—	Filter.HasBasis ENNReal uniformity PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal setOf Preorder.toLE EDist.edist PseudoEMetricSpace.toEDist	—	EMetric.mk_uniformity_basis_le le_refl
uniformity_basis_edist_le' 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Filter.HasBasis ENNReal uniformity PseudoEMetricSpace.toUniformSpace Set Set.instMembership Set.Ioo PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal setOf Preorder.toLE EDist.edist PseudoEMetricSpace.toEDist	—	EMetric.mk_uniformity_basis_le exists_between ENNReal.instDenselyOrdered lt_min lt_of_le_of_lt min_le_right min_le_left
uniformity_basis_edist_nnreal 📖	mathematical	—	Filter.HasBasis NNReal uniformity PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero setOf ENNReal ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist ENNReal.ofNNReal	—	EMetric.mk_uniformity_basis ENNReal.coe_pos ENNReal.lt_iff_exists_nnreal_btwn le_of_lt
uniformity_basis_edist_nnreal_le 📖	mathematical	—	Filter.HasBasis NNReal uniformity PseudoEMetricSpace.toUniformSpace Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero setOf ENNReal Preorder.toLE ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist ENNReal.ofNNReal	—	EMetric.mk_uniformity_basis_le ENNReal.coe_pos ENNReal.lt_iff_exists_nnreal_btwn le_of_lt
uniformity_dist_of_mem_uniformity 📖	mathematical	Set Filter Filter.instMembership Set.instMembership	iInf Filter Filter.instInfSet Filter.principal setOf	—	Filter.HasBasis.eq_biInf
uniformity_edist 📖	mathematical	—	uniformity PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace iInf Filter ENNReal Filter.instInfSet Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Filter.principal setOf EDist.edist PseudoEMetricSpace.toEDist	—	PseudoEMetricSpace.uniformity_edist
uniformity_pseudoedist 📖	mathematical	—	uniformity PseudoEMetricSpace.toUniformSpace iInf Filter ENNReal Filter.instInfSet Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Filter.principal setOf EDist.edist PseudoEMetricSpace.toEDist	—	PseudoEMetricSpace.uniformity_edist
zero_eq_edist 📖	mathematical	—	ENNReal instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	edist_eq_zero

---

← Back to Index