Theorems · Theorem · combinatorics

SimpleGraph.unreduced_edges_subset

∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  {P : Finpartition A} {G : SimpleGraph α} [inst_3 : DecidableRel G.Adj] {ε : 𝕜},
  {x ∈ A ×ˢ A |
      match x with
      | (x, y) => G.Adj x y ∧ ¬(SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).Adj x y} ⊆
    ((P.nonUniforms G (ε / 8)).biUnion fun x =>
          match x with
          | (U, V) => U ×ˢ V) ∪
        P.parts.biUnion Finset.offDiag ∪
      (P.sparsePairs G (ε / 4)).biUnion fun x =>
        match x with
        | (U, V) => G.interedges U V

Defined in

Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Cited by

1 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderDecidableEqDecidableRel