singletonFinsubgraph_le_adj_left — Mathlib

English

A singleton subgraph at a vertex u is contained in the finsubgraph obtained from an adjacency edge e.

Русский

Подграф-синглтон над вершиной u содержится в подграфе finsubgraph, получаемом из ребра смежности e.

LaTeX

$$$$ \\text{singletonFinsubgraph } u \\leq \\text{finsubgraphOfAdj } e. $$$$

Lean4

theorem singletonFinsubgraph_le_adj_left {u v : V} {e : G.Adj u v} : singletonFinsubgraph u ≤ finsubgraphOfAdj e := by
  simp [singletonFinsubgraph, finsubgraphOfAdj]

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