sSup_adj — Mathlib

English

The edge a–b exists in the supremum of a family s of graphs iff some graph in s contains the edge.

Русский

Ребро a–b существует в верхнем ограничении множества графов iff некоторый граф из s содержит ребро.

LaTeX

$$$ (\mathrm{sup}\ s).Adj a b \iff \exists G \in s,\ G.Adj a b $$$

Lean4

@[simp]
theorem sSup_adj {s : Set (SimpleGraph V)} {a b : V} : (sSup s).Adj a b ↔ ∃ G ∈ s, Adj G a b :=
  Iff.rfl

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