range_getVert_eq_range_support_getElem

English

The range of the function p.getVert equals the range of p.support.get.

Русский

Область значений p.getVert совпадает с областью значений p.support.get.

LaTeX

$$$ \mathrm{range}(p.\text{getVert}) = \mathrm{range}(p.\text{support}.\text{get}) $$$

Lean4

theorem range_getVert_eq_range_support_getElem {u v : V} (p : G.Walk u v) :
    Set.range p.getVert = Set.range p.support.get :=
  Set.ext fun _ ↦
    ⟨by grind [Set.range_list_get, getVert_mem_support], fun ⟨n, _⟩ ↦
      ⟨n, by grind [getVert_eq_support_getElem, length_support]⟩⟩

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