decidablePred — Mathlib

English

If a graph is locally finite at a vertex, then so is a subgraph of that graph at the same vertex.

Русский

Если граф локально конечен в вершине, то и подграф того же графа в той же вершине локально конечен.

LaTeX

$$$\text{instance }\text{finiteAt} {G' : \text{Subgraph}(G)}(v : G'.verts) \ [DecidableRel G'.Adj] [Fintype (G.neighborSet v)] : Fintype (G'.neighborSet v).$$$

Lean4

instance decidablePred (G' : Subgraph G) [h : DecidableRel G'.Adj] (v : V) : DecidablePred (· ∈ G'.neighborSet v) :=
  h v

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