mem_coe_supp_of_adj — Mathlib

English

If a point in a coerced component image corresponds to an adjacency relation, its image lies in the target component’s image.

Русский

Если точка в образе компоненты по существованию через приведение относится к отношению смежности, её образ принадлежит образу целевой компоненты.

LaTeX

$$theorem mem_coe_supp_of_adj {v w : V} {H : Subgraph G} {c : ConnectedComponent H.coe} (hv : v ∈ (↑) '' (c : Set H.verts)) (hw : w ∈ H.verts) (hadj : H.Adj v w) : w ∈ (↑) '' (c : Set H.verts) := ...$$

Lean4

theorem mem_coe_supp_of_adj {v w : V} {H : Subgraph G} {c : ConnectedComponent H.coe}
    (hv : v ∈ (↑) '' (c : Set H.verts)) (hw : w ∈ H.verts) (hadj : H.Adj v w) : w ∈ (↑) '' (c : Set H.verts) :=
  by
  obtain ⟨_, h⟩ := hv
  use ⟨w, hw⟩
  rw [← (mem_supp_iff _ _).mp h.1]
  exact ⟨connectedComponentMk_eq_of_adj <| Subgraph.Adj.coe <| h.2 ▸ hadj.symm, rfl⟩

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