mem_support_iff — Mathlib

English

An element w belongs to the support of p if and only if w = u or w belongs to the tail of p.support.

Русский

Элемент w принадлежит опоре p тогда и только тогда, когда w = u или w ∈ p.support.tail.

LaTeX

$$$w \in p.\mathrm{support} \iff w = u \lor w \in p.\mathrm{support}.\mathrm{tail}$$$

Lean4

theorem mem_support_iff {u v w : V} (p : G.Walk u v) : w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail := by cases p <;> simp

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