Theorems · Theorem · combinatorics

SimpleGraph.extremalNumber_congr

∀ {n₁ n₂ : ℕ} {W₁ : Type u_4} {W₂ : Type u_5} {H₁ : SimpleGraph W₁} {H₂ : SimpleGraph W₂},
  n₁ = n₂ → ∀ (e : H₁ ≃g H₂), SimpleGraph.extremalNumber n₁ H₁ = SimpleGraph.extremalNumber n₂ H₂

If H₁ ≃g H₂, then extremalNumber n H₁ equals extremalNumber n H₂.

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Cited by

1 results in Mathlib

Foundations

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