sSup_adj — Mathlib

English

Let s be a set of subgraphs of G. Then a is adjacent to b in the supremum of s iff there exists a subgraph G in s for which a and b are adjacent.

Русский

Пусть s – множество подграфов графа G. Тогда a и b смежны в наибольшем подграфе s тогда и только тогда, когда существует подграф G ∈ s, в котором a и b смежны.

LaTeX

$$$ (sSup s).Adj a b \\iff \\exists G \\in s, Adj\\, G\\, a\\, b $$$

Lean4

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

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