PairReduction

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

Statistics

Metric	Count
Definitions logSizeBallSeq, logSizeBallStruct, ball, finset, point, radius, smallBall, logSizeRadius, pairSet, pairSetSeq	10
Theorems pair_reduction, antitone_logSizeBallSeq_add_one_subset, card_finset_logSizeBallSeq_add_one_lt, card_finset_logSizeBallSeq_card_eq_zero, card_finset_logSizeBallSeq_le, card_le_logSizeRadius_le_pow_logSizeRadius, card_pairSetSeq_le_logSizeRadius_mul, card_pairSet_le, disjoint_smallBall_logSizeBallSeq, edist_le_of_mem_pairSet, exists_radius_le, finset_logSizeBallSeq_add_one, finset_logSizeBallSeq_add_one_ssubset, finset_logSizeBallSeq_add_one_subset, finset_logSizeBallSeq_subset_logSizeBallSeq_init, finset_logSizeBallSeq_zero, iSup_edist_pairSet, logSizeRadius_le_card_smallBall, one_le_logSizeRadius, one_le_radius_logSizeBallSeq, pairSet_empty_eq_empty, pairSet_subset, point_logSizeBallSeq_add_one, point_logSizeBallSeq_zero, point_mem_finset_logSizeBallSeq, point_mem_logSizeBallSeq_init, point_notMem_finset_logSizeBallSeq_add_one, pow_logSizeRadius_le_card_le_logSizeRadius, radius_logSizeBallSeq_add_one, radius_logSizeBallSeq_le, radius_logSizeBallSeq_zero	31
Total	41

EMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pair_reduction 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring	Finset Finset.instHasSubset SProd.sprod Finset.instSProd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring EDist.edist PseudoEMetricSpace.toEDist iSup SetLike.instMembership Finset.instSetLike CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice ENNReal.instCompleteLinearOrder instPseudoEMetricSpaceSubtype instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat le_or_gt isEmpty_or_nonempty Finset.product_empty CharP.cast_eq_zero CharP.ofCharZero ENNReal.instCharZero MulZeroClass.mul_zero ENNReal.instCanonicallyOrderedAdd instIsEmptyFalse Finset.card_eq_one le_antisymm LE.le.trans one_pow ENNReal.pow_le_pow_left Nat.cast_one IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing Finset.one_le_card Finset.nonempty_coe_sort Prod.mk_left_injective Finset.product_singleton Finset.map_singleton Finset.card_singleton mul_one ciSup_unique PseudoEMetricSpace.edist_self PairReduction.pairSet_subset PairReduction.card_pairSet_le PairReduction.edist_le_of_mem_pairSet PairReduction.iSup_edist_pairSet

PairReduction

Definitions

Name	Category	Theorems
logSizeBallSeq 📖	CompOp	18 math math: point_notMem_finset_logSizeBallSeq_add_one, card_pairSetSeq_le_logSizeRadius_mul, finset_logSizeBallSeq_zero, point_mem_logSizeBallSeq_init, disjoint_smallBall_logSizeBallSeq, finset_logSizeBallSeq_add_one, card_finset_logSizeBallSeq_le, radius_logSizeBallSeq_add_one, card_finset_logSizeBallSeq_card_eq_zero, one_le_radius_logSizeBallSeq, finset_logSizeBallSeq_add_one_subset, antitone_logSizeBallSeq_add_one_subset, finset_logSizeBallSeq_subset_logSizeBallSeq_init, point_logSizeBallSeq_add_one, point_logSizeBallSeq_zero, logSizeRadius_le_card_smallBall, radius_logSizeBallSeq_le, radius_logSizeBallSeq_zero
logSizeBallStruct 📖	CompData	—
logSizeRadius 📖	CompOp	5 math math: one_le_logSizeRadius, pow_logSizeRadius_le_card_le_logSizeRadius, card_le_logSizeRadius_le_pow_logSizeRadius, radius_logSizeBallSeq_add_one, radius_logSizeBallSeq_zero
pairSet 📖	CompOp	4 math math: pairSet_empty_eq_empty, card_pairSet_le, pairSet_subset, iSup_edist_pairSet
pairSetSeq 📖	CompOp	1 math math: card_pairSetSeq_le_logSizeRadius_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_logSizeBallSeq_add_one_subset 📖	mathematical	Finset.Nonempty	Antitone Finset Nat.instPreorder PartialOrder.toPreorder Finset.partialOrder logSizeBallStruct.finset logSizeBallSeq	—	antitone_nat_of_succ_le finset_logSizeBallSeq_add_one_subset
card_finset_logSizeBallSeq_add_one_lt 📖	mathematical	Finset.Nonempty logSizeBallStruct.finset logSizeBallSeq	Finset.card	—	finset_logSizeBallSeq_add_one_ssubset
card_finset_logSizeBallSeq_card_eq_zero 📖	mathematical	Finset.Nonempty	Finset.card logSizeBallStruct.finset logSizeBallSeq	—	tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub card_finset_logSizeBallSeq_le
card_finset_logSizeBallSeq_le 📖	mathematical	Finset.Nonempty	Finset.card logSizeBallStruct.finset logSizeBallSeq	—	tsub_zero Nat.instOrderedSub card_finset_logSizeBallSeq_add_one_lt le_trans Finset.card_le_card finset_logSizeBallSeq_add_one_subset not_ne_iff Iff.not Finset.card_ne_zero Nat.instCanonicallyOrderedAdd
card_le_logSizeRadius_le_pow_logSizeRadius 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Preorder.toLE AddMonoidWithOne.toNatCast Finset.card Finset.filter EDist.edist PseudoEMetricSpace.toEDist Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring logSizeRadius LinearOrder.toDecidableLE ENNReal.instLinearOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	exists_radius_le logSizeRadius.eq_1 Nat.find_spec
card_pairSetSeq_le_logSizeRadius_mul 📖	mathematical	Finset.Nonempty ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Preorder.toLE AddMonoidWithOne.toNatCast Finset.card pairSetSeq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring logSizeBallStruct.finset logSizeBallSeq Finset.decidableNonempty instZeroENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero logSizeBallStruct.radius	—	Prod.mk_right_injective Finset.singleton_product Finset.card_map one_mul card_le_logSizeRadius_le_pow_logSizeRadius Finset.filter.congr_simp Finset.filter_empty Finset.product_empty CharP.cast_eq_zero CharP.ofCharZero ENNReal.instCharZero MulZeroClass.zero_mul
card_pairSet_le 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Preorder.toLE AddMonoidWithOne.toNatCast Finset.card pairSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	le_imp_le_of_le_of_le Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing Finset.card_biUnion_le le_refl Nat.cast_sum Finset.sum_le_sum card_pairSetSeq_le_logSizeRadius_mul mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid pow_le_pow_right₀ IsOrderedRing.toPosMulMono LT.lt.le le_tsub_add Nat.instOrderedSub pow_add pow_one mul_assoc mul_comm Finset.mul_sum logSizeRadius_le_card_smallBall Finset.card_biUnion disjoint_smallBall_logSizeBallSeq Finset.card_le_card Finset.biUnion_subset_iff_forall_subset HasSubset.Subset.trans Finset.instIsTransSubset Finset.filter_subset finset_logSizeBallSeq_subset_logSizeBallSeq_init Finset.not_nonempty_iff_eq_empty CharP.cast_eq_zero CharP.ofCharZero ENNReal.instCharZero MulZeroClass.mul_zero
disjoint_smallBall_logSizeBallSeq 📖	mathematical	Finset.Nonempty	Disjoint Finset Finset.partialOrder Finset.instOrderBot logSizeBallStruct.smallBall logSizeBallSeq	—	Finset.disjoint_of_subset_right HasSubset.Subset.trans Finset.instIsTransSubset Finset.filter_subset antitone_logSizeBallSeq_add_one_subset Disjoint.symm ne_iff_lt_iff_le
edist_le_of_mem_pairSet 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Preorder.toLE AddMonoidWithOne.toNatCast Finset.card Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring Finset Finset.instMembership pairSet	EDist.edist PseudoEMetricSpace.toEDist Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Finset.card_pos Prod.mk_right_injective Finset.singleton_product le_imp_le_of_le_of_le le_refl mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing radius_logSizeBallSeq_le Finset.mem_product pairSet_subset Finset.card_le_one_iff pow_zero ENNReal.instCharZero PseudoEMetricSpace.edist_self zero_le ENNReal.instCanonicallyOrderedAdd
exists_radius_le 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Preorder.toLE AddMonoidWithOne.toNatCast Finset.card Finset.filter EDist.edist PseudoEMetricSpace.toEDist Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring LinearOrder.toDecidableLE ENNReal.instLinearOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	ENNReal.tendsto_nhds_top_iff_nat Filter.Tendsto.comp ENNReal.tendsto_rpow_atTop_of_one_lt_base tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean ENNReal.rpow_natCast instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat le_max_right le_trans IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero Finset.card_filter_le LT.lt.le le_max_left
finset_logSizeBallSeq_add_one 📖	mathematical	Finset.Nonempty	logSizeBallStruct.finset logSizeBallSeq Finset Finset.instSDiff logSizeBallStruct.smallBall	—	—
finset_logSizeBallSeq_add_one_ssubset 📖	mathematical	Finset.Nonempty logSizeBallStruct.finset logSizeBallSeq	Finset Finset.instHasSSubset	—	ssubset_of_subset_not_subset Finset.instIsNonstrictStrictOrderSubsetSSubset Set.not_subset point_mem_finset_logSizeBallSeq point_notMem_finset_logSizeBallSeq_add_one
finset_logSizeBallSeq_add_one_subset 📖	mathematical	Finset.Nonempty	Finset Finset.instHasSubset logSizeBallStruct.finset logSizeBallSeq	—	—
finset_logSizeBallSeq_subset_logSizeBallSeq_init 📖	mathematical	Finset.Nonempty	Finset Finset.instHasSubset logSizeBallStruct.finset logSizeBallSeq	—	subset_trans Finset.instIsTransSubset antitone_logSizeBallSeq_add_one_subset zero_le Nat.instCanonicallyOrderedAdd Finset.instReflSubset
finset_logSizeBallSeq_zero 📖	mathematical	Finset.Nonempty	logSizeBallStruct.finset logSizeBallSeq	—	—
iSup_edist_pairSet 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Preorder.toLE iSup Finset SetLike.instMembership Finset.instSetLike CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice ENNReal.instCompleteLinearOrder EDist.edist PseudoEMetricSpace.toEDist instPseudoEMetricSpaceSubtype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat pairSet	—	Nat.instAtLeastTwoHAddOfNat iSup_le_iff Nat.findGreatest_spec zero_le Nat.instCanonicallyOrderedAdd le_imp_le_of_le_of_le le_refl mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid tsub_le_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub le_trans PseudoEMetricSpace.edist_triangle add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add one_mul add_mul Distrib.rightDistribClass ENNReal.sub_add_eq_add_sub Nat.cast_one Nat.mono_cast IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing one_le_radius_logSizeBallSeq ENNReal.one_ne_top ENNReal.add_sub_cancel_right Prod.mk_right_injective Finset.singleton_product iSup_subtype iSup_congr_Prop le_iSup_of_le Finset.mem_biUnion Finset.mem_range lt_of_le_of_lt Nat.findGreatest_le Finset.card_pos zero_lt_one Nat.instZeroLEOneClass le_rfl two_mul PseudoEMetricSpace.edist_comm Order.one_le_iff_pos add_le_add_left Nat.instIsOrderedAddMonoid Nat.instOrderedSub Finset.card_eq_zero card_finset_logSizeBallSeq_le Nat.findGreatest_is_greatest lt_add_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd logSizeBallSeq.congr_simp Nat.findGreatest.congr_simp
logSizeRadius_le_card_smallBall 📖	mathematical	Finset.Nonempty ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring logSizeBallStruct.finset logSizeBallSeq Finset.decidableNonempty instZeroENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero logSizeBallStruct.radius AddMonoidWithOne.toNatCast Finset.card logSizeBallStruct.smallBall	—	one_mul pow_logSizeRadius_le_card_le_logSizeRadius point_mem_finset_logSizeBallSeq MulZeroClass.zero_mul ENNReal.instCanonicallyOrderedAdd
one_le_logSizeRadius 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	logSizeRadius	—	exists_radius_le logSizeRadius.eq_1 Nat.find_spec
one_le_radius_logSizeBallSeq 📖	mathematical	Finset.Nonempty ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	logSizeBallStruct.radius logSizeBallSeq	—	one_le_logSizeRadius
pairSet_empty_eq_empty 📖	mathematical	—	pairSet Finset Finset.instEmptyCollection	—	—
pairSet_subset 📖	mathematical	—	Finset Finset.instHasSubset pairSet SProd.sprod Finset.instSProd	—	Finset.biUnion_subset_iff_forall_subset Finset.product_subset_product Finset.singleton_subset_iff point_mem_logSizeBallSeq_init HasSubset.Subset.trans Finset.instIsTransSubset Finset.filter_subset finset_logSizeBallSeq_subset_logSizeBallSeq_init
point_logSizeBallSeq_add_one 📖	mathematical	Finset.Nonempty	logSizeBallStruct.point logSizeBallSeq logSizeBallStruct.finset Finset.decidableNonempty Finset Finset.instMembership	—	—
point_logSizeBallSeq_zero 📖	mathematical	Finset.Nonempty	logSizeBallStruct.point logSizeBallSeq Finset Finset.instMembership	—	—
point_mem_finset_logSizeBallSeq 📖	mathematical	Finset.Nonempty logSizeBallStruct.finset logSizeBallSeq	Finset Finset.instMembership logSizeBallStruct.point	—	—
point_mem_logSizeBallSeq_init 📖	mathematical	Finset.Nonempty	Finset Finset.instMembership logSizeBallStruct.point logSizeBallSeq	—	point_mem_finset_logSizeBallSeq Finset.mem_of_subset finset_logSizeBallSeq_subset_logSizeBallSeq_init
point_notMem_finset_logSizeBallSeq_add_one 📖	mathematical	Finset.Nonempty	Finset Finset.instMembership logSizeBallStruct.finset logSizeBallSeq logSizeBallStruct.point	—	PseudoEMetricSpace.edist_self ENNReal.instCanonicallyOrderedAdd
pow_logSizeRadius_le_card_le_logSizeRadius 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset Finset.instMembership	Preorder.toLE Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring logSizeRadius AddMonoidWithOne.toNatCast Finset.card Finset.filter EDist.edist PseudoEMetricSpace.toEDist Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.instSub LinearOrder.toDecidableLE ENNReal.instLinearOrder	—	tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero Finset.filter.congr_simp Nat.cast_one ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub MulZeroClass.zero_mul IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero PseudoEMetricSpace.edist_self exists_radius_le logSizeRadius.eq_1 IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instIsOrderedAddMonoid CharP.cast_eq_zero CharP.ofCharZero instIsEmptyFalse Nat.instZeroLEOneClass Nat.find_min LT.lt.le ENNReal.natCast_sub
radius_logSizeBallSeq_add_one 📖	mathematical	Finset.Nonempty	logSizeBallStruct.radius logSizeBallSeq logSizeRadius logSizeBallStruct.point logSizeBallStruct.finset	—	—
radius_logSizeBallSeq_le 📖	mathematical	Finset.Nonempty ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Preorder.toLE AddMonoidWithOne.toNatCast Finset.card Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring	logSizeBallStruct.radius logSizeBallSeq	—	exists_radius_le Nat.find_min' le_trans Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing Finset.card_le_card Finset.filter_subset HasSubset.Subset.trans Finset.instIsTransSubset finset_logSizeBallSeq_subset_logSizeBallSeq_init
radius_logSizeBallSeq_zero 📖	mathematical	Finset.Nonempty	logSizeBallStruct.radius logSizeBallSeq logSizeRadius Finset Finset.instMembership	—	—

PairReduction.logSizeBallStruct

Definitions

Name	Category	Theorems
ball 📖	CompOp	—
finset 📖	CompOp	12 math math: PairReduction.point_notMem_finset_logSizeBallSeq_add_one, PairReduction.card_pairSetSeq_le_logSizeRadius_mul, PairReduction.finset_logSizeBallSeq_zero, PairReduction.finset_logSizeBallSeq_add_one, PairReduction.card_finset_logSizeBallSeq_le, PairReduction.radius_logSizeBallSeq_add_one, PairReduction.card_finset_logSizeBallSeq_card_eq_zero, PairReduction.finset_logSizeBallSeq_add_one_subset, PairReduction.antitone_logSizeBallSeq_add_one_subset, PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init, PairReduction.point_logSizeBallSeq_add_one, PairReduction.logSizeRadius_le_card_smallBall
point 📖	CompOp	6 math math: PairReduction.point_notMem_finset_logSizeBallSeq_add_one, PairReduction.point_mem_logSizeBallSeq_init, PairReduction.radius_logSizeBallSeq_add_one, PairReduction.point_mem_finset_logSizeBallSeq, PairReduction.point_logSizeBallSeq_add_one, PairReduction.point_logSizeBallSeq_zero
radius 📖	CompOp	6 math math: PairReduction.card_pairSetSeq_le_logSizeRadius_mul, PairReduction.radius_logSizeBallSeq_add_one, PairReduction.one_le_radius_logSizeBallSeq, PairReduction.logSizeRadius_le_card_smallBall, PairReduction.radius_logSizeBallSeq_le, PairReduction.radius_logSizeBallSeq_zero
smallBall 📖	CompOp	3 math math: PairReduction.disjoint_smallBall_logSizeBallSeq, PairReduction.finset_logSizeBallSeq_add_one, PairReduction.logSizeRadius_le_card_smallBall

---

← Back to Index