Theorems · Theorem · combinatorics

SimpleGraph.regularityReduced_edges_card_aux

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj]
  {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α],
  0 < ε →
    P.IsEquipartition →
      P.IsUniform G (ε / 8) →
        4 / ε ≤ ↑P.parts.card →
          2 * (↑G.edgeFinset.card - ↑(SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).edgeFinset.card) <
            2 * ε * ↑(Fintype.card α ^ 2)

Defined in: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Cited by: 1 results in Mathlib
Foundations: Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Fintype DecidableRel Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites43

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

Realstatement and proof · cited by 25,697
Finsetstatement and proof · cited by 13,712
Fintypestatement and proof · cited by 7,736
Finset.univstatement and proof · cited by 3,473
SimpleGraphstatement and proof · cited by 3,072
Finset.cardstatement and proof · cited by 2,327
le_reflproof · cited by 2,061
SProd.sprodproof · cited by 1,750
Fintype.cardstatement and proof · cited by 1,386
SimpleGraph.Adjstatement and proof · cited by 1,346
le_of_ltproof · cited by 1,175
Finset.filterproof · cited by 949

Cited by1

Results whose statement or proof uses this declaration.

SimpleGraph.FarFromTriangleFree.le_card_cliqueFinsetproof · cited by 2