getVert_nil — Mathlib

English

Let G be a graph on vertex set V. The nil walk starting at a vertex u ∈ V has the property that every position i ∈ ℕ maps to the starting vertex u; i.e., the i-th vertex along the nil walk is u.

Русский

Пусть G — граф на вершинном множестве V. Нулевой путь, начинающийся в вершине u ∈ V, имеет свойство: на каждой позиции i ∈ ℕ i-й элемент пути равен начальной вершине u.

LaTeX

$$$$\forall u \in V, \forall i \in \mathbb{N},\; \text{getVert}(\text{nil}(u), i) = u.$$$$

Lean4

@[simp]
theorem getVert_nil (u : V) {i : ℕ} : (@nil _ G u).getVert i = u :=
  rfl

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