extremalNumber_congr — Mathlib

English

If H1 ≃g H2, then extremalNumber n H1 = 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₂`. -/
@[congr]
theorem extremalNumber_congr {n₁ n₂ : ℕ} {W₁ W₂ : Type*} {H₁ : SimpleGraph W₁} {H₂ : SimpleGraph W₂} (h : n₁ = n₂)
    (e : H₁ ≃g H₂) : extremalNumber n₁ H₁ = extremalNumber n₂ H₂ :=
  by
  rw [h, le_antisymm_iff]
  and_intros
  on_goal 2 => replace e := e.symm
  all_goals
    rw [← Fintype.card_fin n₂, extremalNumber_le_iff]
    intro G _ h
    apply card_edgeFinset_le_extremalNumber
    contrapose! h
    exact h.trans' ⟨e.toCopy⟩

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