Theorems · Theorem · general topology

PairReduction.logSizeBallStruct.mk.injEq

∀ {T : Type u_2} (finset : Finset T) (point : T) (radius : ℕ) (finset_1 : Finset T) (point_1 : T) (radius_1 : ℕ),
  ({ finset := finset, point := point, radius := radius } =
      { finset := finset_1, point := point_1, radius := radius_1 }) =
    (finset = finset_1 ∧ point = point_1 ∧ radius = radius_1)

Defined in: Mathlib.Topology.EMetricSpace.PairReduction
Cited by: 0 results in Mathlib
Foundations: Depth 8 from the axioms · uses propext

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

Finsetstatement and proof · cited by 13,712
PairReduction.logSizeBallStructstatement · cited by 4
PairReduction.logSizeBallStruct.mk.injproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.