Theorems · Theorem · combinatorics

SimpleGraph.zarankiewicz_le_iff

∀ {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : Fintype α] [inst_3 : Fintype β],
  Fintype.card V = m →
    Fintype.card W = n →
      Fintype.card α = s →
        Fintype.card β = t →
          ∀ (x : ℕ),
            SimpleGraph.zarankiewicz m n s t ≤ x ↔
              ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst_4 : DecidableRel G.Adj],
                G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → G.edgeFinset.card ≤ x

zarankiewicz m n s t is at most x if and only if every completeBipartiteGraph α β-free bipartite graph G has at most x edges.

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFintypeFintypeFintype