subset_support_append_right — Mathlib

English

Symmetrically, for p from u to v and q from v to w, q.support is contained in (p.append q).support.

Русский

Аналогично, q.support ⊆ (p.append q).support.

LaTeX

$$$q.\mathrm{support} \subseteq (p.\mathrm{append}\ q).\mathrm{support}$$$

Lean4

@[simp]
theorem subset_support_append_right {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) :
    q.support ⊆ (p.append q).support := by
  intro h
  simp +contextual only [mem_support_append_iff, or_true, imp_true_iff]

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