disjoint_edge — Mathlib

English

For any G and vertices u, v, the edge uv is disjoint from G if and only if u and v are not adjacent in G.

Русский

Для любого графа G и вершин u, v ребро uv является несовместимым с G тогда и только тогда, когда u и v не смежны в G.

LaTeX

$$$Disjoint\\ G\\ (edge\\ u\\ v) \\iff \\neg G.Adj\\ u\\ v$$$

Lean4

theorem disjoint_edge {u v : V} : Disjoint G (edge u v) ↔ ¬G.Adj u v :=
  by
  by_cases h : u = v
  · subst h
    simp [edge_self_eq_bot]
  simp [← disjoint_edgeSet, edge_edgeSet_of_ne h]

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