Mathlib Map

Theorems · Inductive type · general topology

PairReduction.logSizeBallStruct

Type u_2 → Type u_2

A structure for carrying the data of logSizeBallSeq

Defined in
Mathlib.Topology.EMetricSpace.PairReduction
Cited by
4 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PairReduction.logSizeBallSeq · cited by 26PairReduction.logSizeBall…PairReduction.logSizeBallStruct.finset · cited by 22logSizeBallStruct.finsetPairReduction.logSizeBallStruct.point · cited by 15logSizeBallStruct.pointPairReduction.logSizeBallStruct.radius · cited by 12logSizeBallStruct.radiusPairReduction.logSizeBallStruct.smallBall · cited by 4logSizeBallStruct.smallBa…PairReduction.logSizeBallSeq.congr_simp · cited by 1logSizeBallSeq.congr_simpPairReduction.logSizeBallStruct.ball · cited by 1logSizeBallStruct.ballPairReduction.logSizeBallStruct.mk.inj · cited by 1mk.injPairReduction.logSizeBallStruct.mk.noConfusion · cited by 1mk.noConfusionPairReduction.logSizeBallStruct.casesOn · cited by 0logSizeBallStruct.casesOnPairReduction.logSizeBallStruct.ctorIdx · cited by 0logSizeBallStruct.ctorIdxPairReduction.logSizeBallStruct.noConfusion · cited by 0logSizeBallStruct.noConfu…PairReduction.logSizeBallStruct.noConfusionType · cited by 0logSizeBallStruct.noConfu…PairReduction.logSizeBallStruct.recOn · cited by 0logSizeBallStruct.recOnPairReduction.logSizeBallStruct.mk.injEq · cited by 0mk.injEqPairReduction.logSizeBallStru…CITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by16

Results whose statement or proof uses this declaration.