prop — Mathlib

English

A graph G is extremal with respect to a property p if p holds for G and if every other G' with p satisfies #G'.edgeFinset ≤ #G.edgeFinset.

Русский

Граф $G$ экстремален по отношению к свойству $p$, если $p(G)$ выполняется и для любого $G'$ с $p(G')$ выполняется неубывание числа ребер: $|E(G')|\le |E(G)|$.

LaTeX

$$$G.IsExtremal(p) \\iff p(G) \\land \\forall G'\\; [DecidableRel G'.Adj],\\; p(G') \\Rightarrow |G'.edgeFinset| \\le |G.edgeFinset|$$$

Lean4

theorem prop {p : SimpleGraph V → Prop} (h : G.IsExtremal p) : p G :=
  h.1

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