connectedComponentMk_supp_subset_supp

English

If G ≤ G' and c' is a component of G', and v ∈ c'.supp, then the component of v in G has its support contained in c'.supp.

Русский

Если G ≤ G' и c' — компонентa G', и v ∈ c'.supp, то supp(G.connectedComponentMk v) ⊆ c'.supp.

LaTeX

$$$(G.connectedComponentMk v).supp \\\\subseteq c'.supp$$$

Lean4

theorem connectedComponentMk_supp_subset_supp {G'} {v : V} (h : G ≤ G') (c' : G'.ConnectedComponent)
    (hc' : v ∈ c'.supp) : (G.connectedComponentMk v).supp ⊆ c'.supp :=
  by
  intro v' hv'
  simp only [mem_supp_iff, ConnectedComponent.eq] at hv' ⊢
  rw [ConnectedComponent.sound (hv'.mono h)]
  exact hc'

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