Theorems · Theorem · general topology

PairReduction.logSizeBallSeq.congr_simp

∀ {T : Type u_1} [inst : PseudoEMetricSpace T] [inst_1 : DecidableEq T] (J J_1 : Finset T) (e_J : J = J_1)
  (hJ : J.Nonempty) (a a_1 : ENNReal),
  a = a_1 →
    ∀ (c c_1 : ENNReal),
      c = c_1 →
        ∀ (a_2 a_3 : ℕ),
          a_2 = a_3 → PairReduction.logSizeBallSeq J hJ a c a_2 = PairReduction.logSizeBallSeq J_1 ⋯ a_1 c_1 a_3

Defined in: Mathlib.Topology.EMetricSpace.PairReduction
Cited by: 1 results in Mathlib
Foundations: Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoEMetricSpace DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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
ENNRealstatement and proof · cited by 9,879
PseudoEMetricSpacestatement and proof · cited by 1,536
Finset.Nonemptystatement and proof · cited by 1,001
PairReduction.logSizeBallSeqstatement and proof · cited by 26
PairReduction.logSizeBallStructstatement · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

PairReduction.iSup_edist_pairSetproof · cited by 1