pseudoMetricSpacePi 📖 | CompOp | 71 mathmath: Fin.nndist_insertNth_insertNth, nndist_pi_le_iff, Topology.CWComplex.continuousOn, Topology.RelCWComplex.pairwiseDisjoint', IsLowerSet.exists_subset_ball, Real.volume_pi_ball, Topology.RelCWComplex.source_eq, Topology.RelCWComplex.continuousOn, stdSimplex_subset_closedBall, Topology.RelCWComplex.union', diam_stdSimplex, sphere_pi, closedBall_pi', BoxIntegral.Box.nndist_le_distortion_mul, BoxIntegral.TaggedPrepartition.isSubordinate_single, NumberField.canonicalEmbedding.integerLattice.inter_ball_finite, pi_properSpace, nndist_le_pi_nndist, Real.dimH_ball_pi, MeasureTheory.Measure.pi_ball, nndist_single_single, Pi.instIsBoundedSMul', nndist_pi_const, diam_stdSimplex_of_subsingleton, BoxIntegral.Box.dist_le_distortion_mul, Topology.CWComplex.union', dist_pi_le_iff, diam_stdSimplex_le, Topology.CWComplex.source_eq, Topology.CWComplex.pairwiseDisjoint', ball_pi, dist_single_single, MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_pi, dist_pi_lt_iff, Topology.CWComplex.mapsTo', dist_mono_left_pi, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, dist_pi_eq_iff, nndist_pi_const_le, nndist_pi_def, closedBall_pi, Pi.instIsBoundedSMul, Pi.instIsUltrametricDist, MeasureTheory.Measure.pi_closedBall, BoxIntegral.Box.diam_Icc_le_of_distortion_le, MeasureTheory.volume_pi_ball, dist_le_dist_of_le_pi, BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le, Real.dimH_ball_pi_fin, Real.dist_le_of_mem_pi_Icc, MeasureTheory.volume_pi_closedBall, Topology.RelCWComplex.mapsTo, Topology.RelCWComplex.disjointBase', dist_pi_def, dist_anti_right_pi, IsUpperSet.exists_subset_ball, IsUnifLocDoublingMeasure.pi, dist_pi_const, dist_pi_const_le, Fin.dist_insertNth_insertNth, nndist_pi_lt_iff, dist_mono_right_pi, Topology.CWComplex.mapsTo, BoxIntegral.unitPartition.diam_boxIcc, dist_le_pi_dist, dist_inf_sup_pi, Real.volume_pi_closedBall, dist_pi_le_iff', ball_pi', dist_anti_left_pi, nndist_pi_eq_iff
|