toEMetricSpace 📖 | CompOp | 524 mathmath: ContinuousLinearEquiv.antilipschitz, LipschitzWith.max_const, MemHolder.nsmul, Unitization.isometry_inr, NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal, EuclideanGeometry.euclideanHausdorffMeasure_eq, ODE.FunSpace.exists_contractingWith_iterate_next, LightCondensed.isoFinYonedaComponents_hom_apply, EuclideanGeometry.side_angle_side, Real.dimH_of_mem_nhds, NonUnitalIsometricContinuousFunctionalCalculus.isometric, HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn, MeasureTheory.hausdorffMeasure_segment, ConvexOn.continuousOn_tfae, ConcaveOn.locallyLipschitz, MemHolder.holderWith, IsometryEquiv.toRealLinearIsometryEquiv_symm_apply, MemHolder.comp, SchwartzMap.pairing_apply_apply, ApproximatesLinearOn.lipschitz, ProperCone.innerDual_univ, ContinuousLinearMap.integral_apply, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, NumberField.InfinitePlace.isometry_embedding, GromovHausdorff.isometry_optimalGHInjr, MeasureTheory.UniformIntegrable.uniformIntegrable_of_tendstoInMeasure, SchwartzMap.lineDerivOp_fourier_eq, LipschitzWith.lipschitzWith_compLp, LinearMap.adjoint_eq_toCLM_adjoint, LightCondSet.continuous_coinducingCoprod, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, Complex.lipschitz_equivRealProd, IsometryEquiv.toRealLinearIsometryEquiv_apply, LinearMap.isSelfAdjoint_toContinuousLinearMap_iff, LipschitzWith.completion_extension, SchwartzMap.bilinLeftCLM_apply, ODE.FunSpace.range_toContinuousMap, Delone.DeloneSet.isCover_coveringRadius, Real.ediam_eq, Real.dimH_lt_top, MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, CompHausLike.LocallyConstant.adjunction_counit, lintegral_fderiv_lineMap_eq_edist, Real.volume_closedEBall, MeasureTheory.isAddHaarMeasure_hausdorffMeasure, ContinuousLinearMap.isometry_mul_flip, Delone.DeloneSet.mapIsometry_trans, Set.infsep_zero_iff_subsingleton_of_finite, SchwartzMap.laplacianCLM_eq, UpperHalfPlane.isometry_real_vadd, ContDiff.lipschitzWith_of_hasCompactSupport, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn, IsometryEquiv.midpoint_fixed, ContinuousMapZero.isometry_toContinuousMap, ContDiffOn.dimH_image_le, SchwartzMap.compCLMOfContinuousLinearEquiv_apply, HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv, ConcaveOn.locallyLipschitzOn_interior, eHolderNorm_eq_zero, instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast, Perfect.small_diam_splitting, LinearMap.adjoint_toContinuousLinearMap, MemHolder.coe_nnHolderNorm_eq_eHolderNorm, UpperHalfPlane.isometry_vertical_line, MeasureTheory.Integrable.edist_toL1_zero, Complex.isometry_conj, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, WithAbs.isometry_of_comp, SchwartzMap.fourier_lineDerivOp_eq, ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith, SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv, SchwartzMap.smulLeftCLM_real_smul, Real.dimH_univ_eq_finrank, Finset.infsep_pos_iff_nontrivial, HasFiniteFPowerSeriesOnBall.cpolynomialOn, UnitAddTorus.mFourierCoeff_toLp, lipschitzWith_sup_right, Real.dimH_univ, MeasureTheory.tendsto_integral_approxOn_of_measurable, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp, HasFPowerSeriesWithinOnBall.differentiableOn, DomAddAct.instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp, CompHausLike.LocallyConstant.counitApp_app, Condensed.isoFinYonedaComponents_hom_apply, ContinuousLinearMap.antilipschitz_of_isEmbedding, hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall, NumberField.InfinitePlace.Completion.isometry_extensionEmbedding, MeasureTheory.convolution_precompR_apply, SchwartzMap.compSubConstCLM_apply, MeasureTheory.Integrable.norm_toL1, antilipschitzWith_mul_right, Real.ediam_Ioc, LinearMap.exists_antilipschitzWith, ConvexOn.locallyLipschitz, LipschitzWith.dist_left, CompHausLike.LocallyConstant.incl_of_counitAppApp, Delone.DeloneSet.mapIsometry_symm_apply_carrier, HasFPowerSeriesWithinOnBall.analyticOn, LipschitzWith.of_le_add, MeasureTheory.SimpleFunc.nnnorm_approxOn_le, lipschitzOnWith_cfc_fun_of_subset, SchwartzMap.smulLeftCLM_sum, 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, Real.dimH_univ_pi_fin, holderWith_zero_iff, LipschitzWith.projIcc, BoundedContinuousFunction.Lp_nnnorm_le, unitInterval.volume_uIcc, ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt, Real.dimH_ball_pi, Metric.toGlueL_isometry, IsCompactOperator.antilipschitz_of_not_hasEigenvalue, SchwartzMap.smulLeftCLM_fun_neg, lipschitzWith_thickenedIndicator, MeasureTheory.lintegral_edist_triangle, ClosedSubmodule.bot_orthogonal_eq_top, MeasureTheory.hausdorffMeasure_pi_real, SchwartzMap.pairing_apply, unitInterval.volume_uIoo, Set.Finite.infsep_pos_iff_nontrivial, StandardSubspace.IsSeparating, MeasureTheory.Measure.hausdorffMeasure_smul₀, MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset, MonotoneOn.locallyBoundedVariationOn, MeasureTheory.lintegral_edist_lt_top, BoundedVariationOn.sub_le, IsPicardLindelof.lipschitzOnWith, MeasureTheory.hasFDerivAt_convolution_right_with_param, MeasureTheory.hasFiniteIntegral_iff_edist, SchwartzMap.postcompCLM_apply, HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt, HasCompactSupport.hasFDerivAt_convolution_right, isometry_cfcₙHom, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, HasStrictFDerivAt.exists_lipschitzOnWith, ClosedSubmodule.top_orthogonal_eq_bot, Complex.antilipschitz_equivRealProd, Complex.isometry_ofReal, lipschitzWith_one_norm', LocallyLipschitz.max, MeasureTheory.SimpleFunc.norm_approxOn_y₀_le, CompHausLike.LocallyConstant.counit_app_hom_app, ContDiff.euclidean_dist, MeasureTheory.SimpleFunc.memLp_approxOn_range, DilationEquiv.mulRight_symm_apply, algebraMap_isometry, hasFDerivAt_integral_of_dominated_loc_of_lip', MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, IsUpperSet.thickening', DilationEquiv.mulLeft_symm_apply, IsometryEquiv.map_midpoint, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, SchwartzMap.compCLMOfAntilipschitz_apply, SchwartzMap.fourierInv_apply_eq, SchwartzMap.smulRightCLM_apply_apply, 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, SchwartzMap.postcompCLM_postcompCLM, Real.lipschitzWith_sin, SchwartzMap.smulLeftCLM_const, Matrix.exp_sum_of_commute, Set.infsep_pos_iff_nontrivial_of_finite, MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm, lipschitzOnWith_cfc_fun, ContinuousLinearEquiv.dimH_image, MeasureTheory.hausdorffMeasure_prod_real, MemHolder.add, Orientation.areaForm'_apply, MeasureTheory.hausdorffMeasure_lineMap_image, AffineMap.lipschitzWith_of_finiteDimensional, ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective, 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, SchwartzMap.fourierMultiplierCLM_apply, LipschitzOnWith.extend_real, SchwartzMap.compSubConstCLM_zero, UniformSpace.Completion.coe_isometry, LipschitzWith.coordinate, HasFiniteFPowerSeriesOnBall.differentiableOn, LipschitzOnWith.extend_finite_dimension, Delone.DeloneSet.mapIsometry_symm, Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, SchwartzMap.fourierInv_lineDerivOp_eq, LipschitzOnWith.extend_lp_infty, Metric.isPreconnected_eball, MeasureTheory.Lp.lipschitzWith_pos_part, PiNat.exists_lipschitz_retraction_of_isClosed, fourierCoeff_toLp, Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le, LinearMap.isPositive_toContinuousLinearMap_iff, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn', Isometry.completion_extension, MemHolder.smul, LipschitzWith.const_min, SchwartzMap.smulLeftCLM_smulLeftCLM_apply, ContinuousLinearMap.isometry_iff_adjoint_comp_self, GromovHausdorff.ghDist_eq_hausdorffDist, ContinuousLinearMap.opNorm_extend_le, ApproximatesLinearOn.lipschitz_sub, lp.lipschitzWith_one_eval, HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal, Real.dimH_of_nonempty_interior, DilationEquiv.mulRight_apply, lipschitzOnWith_cfcₙ_fun, LocallyLipschitz.min_const, Delone.DeloneSet.mapIsometry_refl, BoundedContinuousFunction.mem_Lp, BoundedContinuousFunction.Lp_norm_le, Matrix.l2_opNNNorm_def, KuratowskiEmbedding.embeddingOfSubset_isometry, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, CompHausLike.LocallyConstant.adjunction_left_triangle, MeasureTheory.euclideanHausdorffMeasure_homothety_image, RCLike.lipschitzWith_re, instIsRiemannianManifoldModelWithCornersSelfReal, MeasureTheory.euclideanHausdorffMeasure_homothety_preimage, SchwartzMap.smulLeftCLM_add, BoundedVariationOn.stieltjesFunctionRightLim_apply, Condensed.isoFinYonedaComponents_inv_comp, MeasureTheory.hausdorffMeasure_homothety_image, ContinuousMultilinearMap.integral_apply, UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal, ApproximatesLinearOn.antilipschitz, Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt, IsUpperSet.thickening, CondensedSet.continuous_coinducingCoprod, EuclideanGeometry.similar_of_side_angle_side, GromovHausdorff.AuxGluingStruct.isom, Real.lipschitzWith_one_mulExpNegMulSq, ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range, HasFiniteFPowerSeriesOnBall.continuousOn, MeasureTheory.SimpleFunc.memLp_approxOn, memHolder_iff_holderWith, IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero, ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff, EuclideanGeometry.measurePreserving_vaddConst, ContDiff.locallyLipschitz, HasFTaylorSeriesUpToOn.exists_lipschitzOnWith, MeasureTheory.MeasuredSets.lipschitzWith_measureReal, SchwartzMap.compSubConstCLM_comp, eHolderNorm_nsmul, LipschitzWith.dist_right, ConvexOn.locallyLipschitzOn_iff_continuousOn, HasFPowerSeriesOnBall.analyticOnNhd, Real.Convex.dimH_eq_finrank_vectorSpan, Set.Finite.infsep_zero_iff_subsingleton, variationOnFromTo.sub_self_monotoneOn, ClosedSubmodule.orthogonal_eq_top_iff, Real.volume_eball, LipschitzWith.completion_map, Real.volume_le_diam, MeasureTheory.L1.dist_def, Module.Basis.parallelepiped_eq_map, NumberField.InfinitePlace.isometry_embedding_of_isReal, FormalMultilinearSeries.analyticOnNhd, LipschitzOnWith.extend_pi, MeasureTheory.hausdorffMeasure_smul_right_image, ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt, LipschitzOnWith.coordinate, Real.dimH_univ_pi, LipschitzOnWith.iff_le_add_mul, Metric.isCompact_closure_iff_exists_finite_isCover, isConformalMap_complex_linear_conj, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp, SchwartzMap.tsupport_smulLeftCLM_subset, lipschitzWith_negPart, ContinuousMap.coe_toLp, Real.lipschitzWith_toNNReal, DomMulAct.instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp, antilipschitz_of_bound_of_norm_one, MeasureTheory.SimpleFunc.integrable_approxOn_range, ContinuousLinearMap.intervalIntegral_apply, ConvexOn.locallyLipschitzOn_interior, SchwartzMap.smulLeftCLM_neg, 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, ClosedSubmodule.inf_orthogonal_eq_bot, EuclideanGeometry.similar_of_angle_angle, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz, SchwartzMap.pairing_continuous_left, lipschitzOnWith_cfcₙ_fun_of_subset, SchwartzMap.integralCLM_apply, ProbabilityTheory.condExp_ae_eq_integral_condDistrib', SchwartzMap.lineDerivOp_fourierInv_eq, HasFPowerSeriesOnBall.unique, AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp, Metric.isometry_inl, LocallyLipschitz.max_const, LipschitzWith.iff_le_add_mul, Real.dimH_ball_pi_fin, 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, MemHolder.nnHolderNorm_add_le, SchwartzMap.compCLM_apply, TemperedDistribution.fourierMultiplierCLM_apply_apply, Dilation.ratio_comp, Isometry.isometry_mapRingHom, MeasureTheory.SimpleFunc.integrable_approxOn, ConvexOn.locallyLipschitzOn, Metric.toGlueR_isometry, Submodule.lipschitzWith_starProjection, Real.volume_pi_le_diam_pow, Finset.infsep_zero_iff_subsingleton, MeasureTheory.hausdorffMeasure_real, LipschitzOnWith.of_le_add, SchwartzMap.fderivCLM_fourier_eq, SchwartzMap.derivCLM_apply, Matrix.toLin_finTwoProd_toContinuousLinearMap, Metric.contractibleSpace_eball, ConcaveOn.locallyLipschitzOn, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, WithLp.volume_preserving_ofLp, Metric.isConnected_closedEBall, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, GromovHausdorff.toGHSpace_lipschitz, NonUnitalStarAlgHom.isometry, IsometryEquiv.coeFn_toRealAffineIsometryEquiv, IsLowerSet.thickening, ContDiffOn.exists_lipschitzOnWith, LinearMap.isStarProjection_toContinuousLinearMap_iff, eHolderNorm_add_le, MeasureTheory.dist_integral_le_lintegral_edist, dimH_orthogonalProjection_le, ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt, Convex.lipschitzWith_gauge, ConcaveOn.exists_lipschitzOnWith_of_isBounded, MeasureTheory.lintegral_enorm_eq_lintegral_edist, ContinuousLinearEquiv.dimH_univ, HasFPowerSeriesWithinOnBall.unique, MeasureTheory.SimpleFunc.norm_approxOn_zero_le, hasFDerivAt_integral_of_dominated_of_fderiv_le, EuclideanGeometry.angle_side_angle, RCLike.lipschitzWith_ofReal, Module.Basis.parallelepiped_map, LocallyLipschitz.const_min, ConvexOn.exists_lipschitzOnWith_of_isBounded, Metric.lipschitz_infDist_pt, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, Real.dimH_segment, EuclideanGeometry.angle_angle_side, Submodule.lipschitzWith_orthogonalProjection, EuclideanGeometry.side_side_side, lipschitzWith_of_nnnorm_deriv_le, Real.lipschitzWith_cos, Metric.lipschitz_infDist, NormedSpace.continuousOn_exp, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, MeasureTheory.hausdorffMeasure_affineSegment, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, Metric.eball_contractible, IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero_symm, HolderWith.nnholderNorm_le, MonotoneOn.eVariationOn_le, MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz, Metric.isPathConnected_eball, Dilation.mulRight_toFun, MeasureTheory.BoundedContinuousFunction.inner_toLp, tendsto_measure_cthickening_of_isCompact, Metric.contractibleSpace_closedEBall, ContDiff.dimH_range_le, NNReal.isometry_coe, SchwartzMap.tsupport_derivCLM_subset, HasFPowerSeriesOnBall.continuousOn, ContinuousLinearEquiv.dimH_preimage, ConcaveOn.continuousOn_tfae, lp.isometry_single, CompHausLike.LocallyConstant.unit_app, Delone.DeloneSet.isSeparated_packingRadius, LipschitzOnWith.of_le_add_mul', Metric.lipschitz_infDist_set, Unitization.antilipschitzWith_addEquiv, ClosedSubmodule.orthogonal_disjoint, Metric.Sigma.isometry_mk, IsUpperSet.cthickening', SchwartzMap.smulLeftCLM_sub, SchwartzMap.smulLeftCLM_apply_apply, Real.hausdorffMeasure_of_finrank_lt, SchwartzMap.fourier_fderivCLM_eq, 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, CompHausLike.LocallyConstant.incl_comap, MeasureTheory.isometry_lpMeasSubgroupToLpTrim, InnerProductSpace.euclideanHausdorffMeasure_eq_volume, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, Module.Basis.opNNNorm_le, LinearMap.antilipschitz_of_comap_nhds_le, SchwartzMap.smulLeftCLM_ofReal, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith, IsLowerSet.thickening', lipschitzWith_one_nnnorm', KuratowskiEmbedding.exists_isometric_embedding, Metric.isConnected_eball, Complex.edist_of_re_eq, EuclideanSpace.euclideanHausdorffMeasure_eq_volume, Complex.exists_cthickening_tendstoUniformlyOn, Module.Basis.opNorm_le, isConformalMap_complex_linear, unitInterval.volume_uIoc, lipschitzWith_max, SchwartzMap.smulLeftCLM_apply, MeasureTheory.Measure.euclideanHausdorffMeasure_smul₀, Metric.isometry_inr, MeasureTheory.isAddHaarMeasure_euclideanHausdorffMeasure, lipschitzWith_lineMap, Dilation.mulLeft_toFun, SchwartzMap.smulLeftCLM_compL_smulLeftCLM, MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm, Unitization.lipschitzWith_addEquiv, Complex.edist_of_im_eq, TemperedDistribution.derivCLM_apply_apply, NormedSpace.exp_sum_of_commute, IsometricContinuousFunctionalCalculus.isometric, MeasureTheory.hausdorffMeasure_homothety_preimage, MeasureTheory.ContinuousMap.inner_toLp, lipschitzWith_posPart, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn', NumberField.InfinitePlace.LiesOver.isometry_algebraMap, Matrix.l2_opNorm_def, isometry_induced, MeasureTheory.tendsto_integral_norm_approxOn_sub, 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, SchwartzMap.fourier_convolution, eHolderNorm_smul, ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz, EuclideanSpace.edist_eq, ApproximatesLinearOn.lipschitzOnWith, LipschitzWith.const_max, UniformSpace.Completion.edist_eq, FormalMultilinearSeries.continuousOn, ContDiffAt.exists_lipschitzOnWith, ContDiffWithinAt.exists_lipschitzOnWith, lipschitzWith_min, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite, 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, MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm, IsUniformEmbedding.to_isometry, MeasureTheory.Lp.isometry_compMeasurePreserving, SchwartzMap.smulLeftCLM_smul, MemHolder.smul_iff, ODE.FunSpace.lipschitzWith, ConcaveOn.locallyLipschitzOn_iff_continuousOn, LocallyLipschitz.min, Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le, MeasureTheory.Measure.euclideanHausdorffMeasure_def, LipschitzWith.of_le_add_mul', RCLike.lipschitzWith_im, ContinuousMap.idealOpensGI_choice, HasCompactSupport.hasFDerivAt_convolution_left, TemperedDistribution.smulLeftCLM_apply_apply, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm, BoundedContinuousFunction.lintegral_le_edist_mul, Real.ediam_Icc, CompHausLike.LocallyConstant.adjunction_unit, IsUpperSet.cthickening, ConvexOn.lipschitzOnWith_of_abs_le, HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt, StarAlgEquiv.isometry, Delone.DeloneSet.mapIsometry_apply_carrier, hasFDerivAt_integral_of_dominated_loc_of_lip, 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, lipschitzWith_one_norm, ConcaveOn.lipschitzOnWith_of_abs_le, IsCoercive.antilipschitz, MeasureTheory.edist_integral_le_lintegral_edist
|