finiteAt — Mathlib

English

If G' ≤ G'' and G'' is locally finite at v, then G' is locally finite at v.

Русский

Если G' ⊆ G'' и G'' локально конечен в v, то и G' локально кончен в v.

LaTeX

$$$\forall {G' \le G''} (v : G'.verts) [Fintype (G''.neighborSet v)] : Fintype (G'.neighborSet v).$$$

Lean4

/-- If a graph is locally finite at a vertex, then so is a subgraph of that graph. -/
instance finiteAt {G' : Subgraph G} (v : G'.verts) [DecidableRel G'.Adj] [Fintype (G.neighborSet v)] :
    Fintype (G'.neighborSet v) :=
  Set.fintypeSubset (G.neighborSet v) (G'.neighborSet_subset v)

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