mem_finsetWalkLengthLT_iff — Mathlib

English

p belongs to the length-less-than-n finset iff p.length < n.

Русский

p принадлежит множеству ходов длины менее n тогда и только тогда, когда длина p меньше n.

LaTeX

$${p ∈ G.finsetWalkLengthLT n u v} ↔ p.length < n$$

Lean4

theorem mem_finsetWalkLengthLT_iff {n : ℕ} {u v : V} {p : G.Walk u v} : p ∈ G.finsetWalkLengthLT n u v ↔ p.length < n :=
  Set.ext_iff.mp (G.coe_finsetWalkLengthLT_eq n u v) p

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