neighborSetFintype — Mathlib

English

For each vertex v, the neighbor set G.neighborSet(v) is a finite type (i.e., finite).

Русский

Для каждой вершины v множество соседей G.neighborSet(v) конечно.

LaTeX

$$∃ Fintype (G.neighborSet v).Elem (i.e., G.neighborSet v is finite)$$

Lean4

instance neighborSetFintype [DecidableRel G.Adj] (v : V) : Fintype (G.neighborSet v) :=
  @Subtype.fintype _ (· ∈ G.neighborSet v)
    (by
      simp_rw [mem_neighborSet]
      infer_instance)
    _

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