Theorems · Theorem · combinatorics

SimpleGraph.two_mul_extremalNumber_le_zarankiewicz_symm

∀ {n s t : ℕ} {α : Type u_3} {β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β] [Nonempty α] [Nonempty β],
  Fintype.card α = s →
    Fintype.card β = t →
      2 * SimpleGraph.extremalNumber n (completeBipartiteGraph α β) ≤ SimpleGraph.zarankiewicz n n s t

The symmetric Zarankiewicz function is at least twice a corresponding extremal number.

Defined in: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
Cited by: 0 results in Mathlib
Foundations: Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype Fintype Nonempty Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites39

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

Realproof · cited by 25,697
Finsetproof · cited by 13,712
Fintypestatement and proof · cited by 7,736
Set.Elemproof · cited by 7,166
SimpleGraphproof · cited by 3,072
Finset.cardproof · cited by 2,327
Fintype.cardstatement and proof · cited by 1,386
SimpleGraph.Adjproof · cited by 1,346
Sym2proof · cited by 737
Eq.leproof · cited by 605
Int.cast_natCastproof · cited by 393
Nat.cast_mulproof · cited by 309

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.