deleteVerts_adj — Mathlib

English

The adjacency in the deleted-vertices subgraph satisfies (G'.deleteVerts s).Adj u v iff u and v are in G'.verts, neither is in s, and G'.Adj u v holds.

Русский

Смежность в подграфе после удаления вершин: (G'.deleteVerts s).Adj u v эквивалентно тому, что u и v принадлежат G'.verts, u и v не принадлежат s, и G'.Adj u v истинно.

LaTeX

$$$ (G'.deleteVerts s).Adj u v \;\iff\; u \in G'.verts \land u \notin s \land v \in G'.verts \land v \notin s \land G'.Adj u v $$$

Lean4

theorem deleteVerts_adj {u v : V} :
    (G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v := by simp [and_assoc]

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