mem_verts_toSubgraph — Mathlib

English

For a walk p from u to v in G, a vertex w belongs to the vertex set of the subgraph induced by p if and only if w appears in the support of p.

Русский

Для обхода p от u к v в G вершина w принадлежит множеству вершин подграфа, индуцированного p, тогда и только тогда w встречается в опорном множестве p.

LaTeX

$$w ∈ p.toSubgraph.verts \iff w ∈ p.support$$

Lean4

theorem mem_verts_toSubgraph (p : G.Walk u v) : w ∈ p.toSubgraph.verts ↔ w ∈ p.support := by
  induction p with
  | nil => simp
  | cons h p' ih =>
    rename_i x y z
    have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support := ⟨by rintro (rfl | h) <;> simp [*], by simp +contextual⟩
    simp [ih, or_assoc, this]

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