map_neighborFinset_induce_of_neighborSet_subset

English

If G.neighborSet v ⊆ s, then the induced neighbor Finset equals the neighbor Finset of v restricted to s.

Русский

Если G.neighborSet v ⊆ s, то индуцированное множество соседей равно соседям вершины v внутри s.

LaTeX

$$((G.induce s).neighborFinset v).map (Embedding.subtype s) = G.neighborFinset v$$

Lean4

theorem map_neighborFinset_induce_of_neighborSet_subset {v : s} (h : G.neighborSet v ⊆ s) :
    ((G.induce s).neighborFinset v).map (.subtype s) = G.neighborFinset v := by
  classical
    rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left, ← map_neighborFinset_induce v] at h

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