mem_support_append_iff — Mathlib

English

The support of the concatenation p.concat p' equals the support of p union the support of p'.

Русский

Опора конкатенации обходов p.concat p' равна объединению опор обходов p и p'.

LaTeX

$$$\mathrm{support}(p\append p') = \mathrm{support}(p) \cup \mathrm{support}(p')$$$

Lean4

@[simp, nolint unusedHavesSuffices]
theorem mem_support_append_iff {t u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support :=
  by
  simp only [mem_support_iff, mem_tail_support_append_iff]
  obtain rfl | h := eq_or_ne t v <;> obtain rfl | h' := eq_or_ne t u <;>
      -- this `have` triggers the unusedHavesSuffices linter:
      (try have := h'.symm) <;>
    simp [*]

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