edgeSet_subgraphOfAdj — Mathlib

English

The edge set of the subgraph of adjacency hvw is the singleton {s(v,w)}.

Русский

Множество ребер подграфа по смежности hvw равно одномерному множество {s(v,w)}.

LaTeX

$$$(G.\\mathrm{subgraphOfAdj}(hvw)).\\mathrm{edgeSet} = \\{ s(v,w) \\}$$$

Lean4

@[simp]
theorem edgeSet_subgraphOfAdj {v w : V} (hvw : G.Adj v w) : (G.subgraphOfAdj hvw).edgeSet = {s(v, w)} :=
  by
  ext e
  refine e.ind ?_
  simp only [eq_comm, Set.mem_singleton_iff, Subgraph.mem_edgeSet, subgraphOfAdj_adj, forall₂_true_iff]

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