finiteAtOfSubgraph — Mathlib

English

If there exists an equivalence between G.neighborSet v and H.neighborSet v, then they are equal when finite.

Русский

Если существует эквивалентность между G.neighborSet v и H.neighborSet v, то при конечности они равны.

LaTeX

$$$\forall v : V,\ H : \text{Subgraph}(G),\ (G.neighborSet v) \simeq (H.neighborSet v) \Rightarrow H.neighborSet v = G.neighborSet v$$$

Lean4

/-- If a subgraph is locally finite at a vertex, then so are subgraphs of that subgraph.

This is not an instance because `G''` cannot be inferred. -/
def finiteAtOfSubgraph {G' G'' : Subgraph G} [DecidableRel G'.Adj] (h : G' ≤ G'') (v : G'.verts)
    [Fintype (G''.neighborSet v)] : Fintype (G'.neighborSet v) :=
  Set.fintypeSubset (G''.neighborSet v) (neighborSet_subset_of_subgraph h v)

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