instFintype — Mathlib

English

For any two vertices u, v, the type of walks from u to v that are paths is finite.

Русский

Для любых вершин u, v множество путей между ними, являющихся путями, образует конечный тип.

LaTeX

$$$\text{Finite}(G.Path(u,v))$$$

Lean4

instance instFintype {u v : V} : Fintype (G.Path u v)
    where
  elems :=
    (univ (α := {p : G.Walk u v | p.IsPath ∧ p.length < Fintype.card V})).map
      ⟨fun p ↦ { val := p.val, property := p.prop.left }, fun _ _ h ↦ SetCoe.ext <| Subtype.mk.injEq .. ▸ h⟩
  complete p := mem_map.mpr ⟨⟨p.val, ⟨p.prop, p.prop.length_lt⟩⟩, ⟨mem_univ _, rfl⟩⟩

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