English
For any p, there exists an extremal graph satisfying p if and only if there exists some graph satisfying p.
Русский
Для любого \(p\) существует экстремальный граф, удовлетворяющий \(p\), тогда и только тогда существует граф, удовлетворяющий \(p\).
LaTeX
$$(\\exists G, \\exists _: DecidableRel G.Adj, G.IsExtremal p) \\iff (\\exists G, p G)$$
Lean4
/-- If one simple graph satisfies `p`, then there exists an extremal graph satisfying `p`. -/
theorem exists_isExtremal_iff_exists (p : SimpleGraph V → Prop) :
(∃ G : SimpleGraph V, ∃ _ : DecidableRel G.Adj, G.IsExtremal p) ↔ ∃ G, p G :=
by
refine ⟨fun ⟨_, _, h⟩ ↦ ⟨_, h.1⟩, fun ⟨G, hp⟩ ↦ ?_⟩
obtain ⟨G', hp', h⟩ := by
apply exists_max_image {G | p G} (#·.edgeFinset)
use G, by simpa using hp
use G', inferInstanceAs (DecidableRel G'.Adj)
exact ⟨by simpa using hp', fun _ _ hp ↦ by convert h _ (by simpa using hp)⟩
