English
Existence of an adjacent boundary edge between a component outside K and a vertex in K.
Русский
Существует граница-ребро между компонентой вне K и вершиной из K.
LaTeX
$$$$ \exists (v,w) \; (v \in C) \land (w \in K) \land G.Adj v w $$$$
Lean4
/-- Assuming `G` is preconnected and `K` not empty, given any connected component `C` outside of `K`,
there exists a vertex `k ∈ K` adjacent to a vertex `v ∈ C`.
-/
theorem exists_adj_boundary_pair (Gc : G.Preconnected) (hK : K.Nonempty) :
∀ C : G.ComponentCompl K, ∃ ck : V × V, ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2 :=
by
refine ComponentCompl.ind fun v vnK => ?_
let C : G.ComponentCompl K := G.componentComplMk vnK
let dis := Set.disjoint_iff.mp C.disjoint_right
by_contra! h
suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
symm
rw [Set.eq_univ_iff_forall]
rintro u
by_contra unC
obtain ⟨p⟩ := Gc v u
obtain ⟨⟨⟨x, y⟩, xy⟩, -, xC, ynC⟩ := p.exists_boundary_dart (C : Set V) (G.componentComplMk_mem vnK) unC
exact ynC (mem_of_adj x y xC (fun yK : y ∈ K => h ⟨x, y⟩ xC yK xy) xy)
