eq_singletonSubgraph_iff_verts_eq

English

For a subgraph H of G and a vertex v, H equals the singleton subgraph at v if and only if the vertex set of H is {v}.

Русский

Для подграфа H графа G и вершины v верно: H = подграф-одиночка на v тогда и только тогда, когда множество вершин H равно {v}.

LaTeX

$$$H = G.singletonSubgraph(v) \\iff H.verts = \\{ v \\}$$$

Lean4

theorem eq_singletonSubgraph_iff_verts_eq (H : G.Subgraph) {v : V} : H = G.singletonSubgraph v ↔ H.verts = { v } :=
  by
  refine ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ ?_⟩
  ext
  · rw [h, singletonSubgraph_verts]
  · simp only [«Prop».bot_eq_false, singletonSubgraph_adj, Pi.bot_apply, iff_false]
    intro ha
    have ha1 := ha.fst_mem
    have ha2 := ha.snd_mem
    rw [h, Set.mem_singleton_iff] at ha1 ha2
    subst_vars
    exact ha.ne rfl

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