card_edgeFinset_deleteIncidenceSet_le_extremalNumber

English

If there exists an isomorphism e between H1 and H2, then extremalNumber with respect to H1 equals that with respect to H2.

Русский

Если существует изоморфизм графов $H_1$ и $H_2$, то экстремальный номер по $H_1$ равен экстремальному номеру по $H_2$.

LaTeX

$$\$ \\forall n, \\forall e: H_1 \\cong H_2, \\ \\mathrm{extremalNumber}(n,H_1)=\\mathrm{extremalNumber}(n,H_2) \$$$

Lean4

/-- If `G` is `H.Free`, then `G.deleteIncidenceSet v` is also `H.Free` and has at most
`extremalNumber (card V-1) H` many edges. -/
theorem card_edgeFinset_deleteIncidenceSet_le_extremalNumber [DecidableEq V] (h : H.Free G) (v : V) :
    #(G.deleteIncidenceSet v).edgeFinset ≤ extremalNumber (card V - 1) H :=
  by
  rw [← card_edgeFinset_induce_compl_singleton, ← @card_unique ({ v } : Set V), ← card_compl_set]
  apply card_edgeFinset_le_extremalNumber
  contrapose! h
  exact h.trans ⟨Copy.induce G { v }ᶜ⟩

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