singletonFinsubgraph_le_adj_right

English

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

Русский

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

LaTeX

$$$$ \\text{singletonFinsubgraph } v \\leq \\text{finsubgraphOfAdj } e, $$$$

Lean4

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

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