extremalNumber_congr_right — Mathlib

English

If H1 ≃g H2, then extremalNumber n H1 equals extremalNumber n H2.

Русский

Если $H_1$ гомеоморфен $H_2$, то экстремальный номер одинаков для обоих при прочих условиях.

LaTeX

$$\$ \\forall n, H_1 \\simeq_g H_2 \\Rightarrow \\mathrm{extremalNumber}(n,H_1)=\\mathrm{extremalNumber}(n,H_2) \$$$

Lean4

/-- If `H₁ ≃g H₂`, then `extremalNumber n H₁` equals `extremalNumber n H₂`. -/
theorem extremalNumber_congr_right {W₁ W₂ : Type*} {H₁ : SimpleGraph W₁} {H₂ : SimpleGraph W₂} (e : H₁ ≃g H₂) :
    extremalNumber n H₁ = extremalNumber n H₂ :=
  extremalNumber_congr rfl e

Похожие утверждения