mem_support_iff_exists_append — Mathlib

English

For a path p, w belongs to p's support iff p can be written as a concatenation q.append r with q and r both paths.

Русский

Для пути p вершина w принадлежит поддержке p тогда и только тогда, когда p может быть записан как q.append r, где q и r — пути.

LaTeX

$$$ w \in p.support \iff \exists q,r:\; q.IsPath \land r.IsPath \land p = q.append r $$$

Lean4

theorem mem_support_iff_exists_append {p : G.Walk u v} (hp : p.IsPath) :
    w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r :=
  by
  refine ⟨fun hw ↦ ?_, fun ⟨q, r, hq, hr, hqr⟩ ↦ p.mem_support_iff_exists_append.mpr ⟨q, r, hqr⟩⟩
  obtain ⟨q, r, hqr⟩ := p.mem_support_iff_exists_append.mp hw
  have : (q.append r).IsPath := hqr ▸ hp
  exact ⟨q, r, this.of_append_left, this.of_append_right, hqr⟩

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