exists_isExtremal_free — Mathlib

English

If a graph H has at least one edge, there exists a graph G that is extremal for H.Free starting from the empty graph.

Русский

Если $H$ имеет хотя бы одну ребро, существует граф $G$, экстремальный по отношению к $H.Free$, начиная с пустого графа.

LaTeX

$$(\\exists G)(\\exists _ : DecidableRel G.Adj, G.IsExtremal H.Free)$$

Lean4

/-- If `H` has at least one edge, then there exists an extremal `H.Free` graph. -/
theorem exists_isExtremal_free {W : Type*} {H : SimpleGraph W} (h : H ≠ ⊥) :
    ∃ G : SimpleGraph V, ∃ _ : DecidableRel G.Adj, G.IsExtremal H.Free :=
  (exists_isExtremal_iff_exists H.Free).mpr ⟨⊥, free_bot h⟩

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