singletonSubgraph_eq_induce — Mathlib

English

For any vertex v in V, the subgraph of G consisting of only v is equal to the induced subgraph of the top subgraph on {v}.

Русский

Пусть v — вершина V. Подграф G, состоящий только из вершины v, равен индуцированному подграфу верхнего подграфа по множеству {v}.

LaTeX

$$$ G.singletonSubgraph\;v = (\top : G.Subgraph).induce \{ v \}$$$

Lean4

theorem singletonSubgraph_eq_induce {v : V} : G.singletonSubgraph v = (⊤ : G.Subgraph).induce { v } := by
  ext <;> simp +contextual [-Set.bot_eq_empty, «Prop».bot_eq_false]

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