mem_verts_of_mem_edge — Mathlib

English

If e ∈ G'.edgeSet and v ∈ e, then v ∈ G'.verts.

Русский

Если e принадлежит G'.edgeSet и v принадлежит e, тогда v принадлежит G'.verts.

LaTeX

$$$e \\in G'.edgeSet \\land v \\in e \\Rightarrow v \\in G'.verts$$$

Lean4

theorem mem_verts_of_mem_edge {G' : Subgraph G} {e : Sym2 V} {v : V} (he : e ∈ G'.edgeSet) (hv : v ∈ e) :
    v ∈ G'.verts := by
  induction e
  rcases Sym2.mem_iff.mp hv with (rfl | rfl)
  · exact G'.edge_vert he
  · exact G'.edge_vert (G'.symm he)

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