sup_edge_of_adj — Mathlib

English

Let G be a simple graph on V and s, t ∈ V with G.Adj s t. Then the join (supremum) of G with the edge s t equals G.

Русский

Пусть G — простой граф на V и s, t ∈ V такие, что G.Adj s t. Тогда объединение графа G и ребра s t по верхней границе равно G.

LaTeX

$$$G.Adj\\, s\\, t \\Rightarrow G \\sqcup edge\\ s\\ t = G$$$

Lean4

theorem sup_edge_of_adj (h : G.Adj s t) : G ⊔ edge s t = G := by
  rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edge_edgeSet_of_ne h.ne, Set.singleton_subset_iff, mem_edgeSet]

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