Theorems · Theorem · combinatorics

SimpleGraph.zarankiewicz_le_iff_of_nonneg

∀ {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 β] {R : Type u_5} [inst_4 : Semiring R] [inst_5 : LinearOrder R]
  [FloorSemiring R],
  Fintype.card V = m →
    Fintype.card W = n →
      Fintype.card α = s →
        Fintype.card β = t →
          ∀ {x : R},
            0 ≤ x →
              (↑(SimpleGraph.zarankiewicz m n s t) ≤ x ↔
                ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst_7 : 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

0 results in Mathlib

Foundations

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

Assumes

FintypeFintypeFintypeFintypeSemiringLinearOrderFloorSemiring