Theorems · Theorem · combinatorics

SimpleGraph.zarankiewicz_of_fintypeCard_eq

∀ {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 →
          SimpleGraph.zarankiewicz m n s t =
            {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x => x.edgeFinset.card

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeFintypeFintypeFintype