adj_spanningCoe_toSimpleGraph — Mathlib

English

Let C be a connected component of G. Then C.toSimpleGraph.spanningCoe.Adj v w is true exactly when v ∈ C.supp and G.Adj v w.

Русский

Пусть C — компонент связности графа G. Тогда C.toSimpleGraph.spanningCoe.Adj v w истинно тогда, когда v ∈ C.supp и G.Adj v w.

LaTeX

$$$ C.toSimpleGraph.spanningCoe.Adj v w \\iff v \\in C.supp \\land G.Adj v w $$$

Lean4

theorem adj_spanningCoe_toSimpleGraph {v w : V} (C : G.ConnectedComponent) :
    C.toSimpleGraph.spanningCoe.Adj v w ↔ v ∈ C.supp ∧ G.Adj v w :=
  by
  apply Iff.intro
  · intro h
    simp_all only [map_adj, SetLike.coe_sort_coe, Subtype.exists, mem_supp_iff]
    obtain ⟨_, a, _, _, h₁, h₂, h₃⟩ := h
    subst h₂ h₃
    exact ⟨a, h₁⟩
  · simp only [toSimpleGraph, map_adj, comap_adj, Embedding.subtype_apply, Subtype.exists, exists_and_left, and_imp]
    intro h hadj
    exact ⟨v, h, w, hadj, rfl, (C.mem_supp_congr_adj hadj).mp h, rfl⟩

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