adj_union — Mathlib

English

A subgraph H is preconnected iff for every pair of vertices in H, there exists a walk in G whose subgraph lies inside H and connects them.

Русский

Пусть подграф H предсвязан тогда и только тогда, когда для любых вершин u,v из H существует обход p в G такой, что p.toSubgraph ≤ H и он соединяет u и v.

LaTeX

$$$ H.Preconnected \iff \forall \{u,v\}, u,v \in H.verts \Rightarrow \exists p : G.Walk u v, p.toSubgraph \le H $$$

Lean4

theorem adj_union {H K : G.Subgraph} (Hconn : H.Connected) (Kconn : K.Connected) {u v : V} (uH : u ∈ H.verts)
    (vK : v ∈ K.verts) (huv : G.Adj u v) : ((⊤ : G.Subgraph).induce { u, v } ⊔ H ⊔ K).Connected :=
  by
  refine ((top_induce_pair_connected_of_adj huv).sup Hconn ?_).sup Kconn ?_
  · exact ⟨u, by simp [uH]⟩
  · exact ⟨v, by simp [vK]⟩

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