English
In a finite graph, given a connected component c, there exists a cycle p whose vertex set equals c.supp.
Русский
В конечном графе существует цикл p, вершины которого совпадают с компонентой c.supp.
LaTeX
$$∃ p : G.Walk, p.IsCycle ∧ p.toSubgraph.verts = c.supp$$
Lean4
theorem exists_cycle_toSubgraph_verts_eq_connectedComponentSupp [Finite V] {c : G.ConnectedComponent} (h : G.IsCycles)
(hv : v ∈ c.supp) (hn : (G.neighborSet v).Nonempty) : ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp :=
by
classical
obtain ⟨w, hw⟩ := hn
obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp ⟨hw, h.reachable_deleteEdges hw⟩
have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
have : p.toSubgraph.verts = c.supp :=
by
obtain ⟨c', hc'⟩ :=
p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp
(by
intro v hv w hadj
refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
have : (G.neighborSet v).Nonempty :=
by
rw [Walk.mem_verts_toSubgraph] at hv
refine (Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)
rw [hp.1.ncard_neighborSet_toSubgraph_eq_two hv]
omega
refine @Classical.ofNonempty _ ?_
rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _), h this,
hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)])
rw [hc']
have : v ∈ c'.supp := by
rw [← hc', Walk.mem_verts_toSubgraph]
exact hvp
simp_all
use p.rotate hvp
rw [← this]
exact ⟨hp.1.rotate _, by simp⟩
