map_neighborFinset_induce — Mathlib

English

For v in s, the induced neighbor Finset equals the intersection of the original neighbor Finset with s.

Русский

Для вершины v в s индуцированное множество соседей равно пересечению исходного множества соседей с s.

LaTeX

$$((G.induce s).neighborFinset v).map ( .subtype (· ∈ s)) = G.neighborFinset v ∩ s.toFinset$$

Lean4

theorem map_neighborFinset_induce [DecidableEq V] (v : s) :
    ((G.induce s).neighborFinset v).map (.subtype (· ∈ s)) = G.neighborFinset v ∩ s.toFinset := by ext; simp

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