toSimpleGraph — Mathlib

English

If a connected component of G is a cycle, its simple-graph image also has cycles.

Русский

Если компонент связности графа G является циклом, соответствующий простой граф имеет циклы.

LaTeX

$$c.toSimpleGraph.spanningCoe.IsCycles$$

Lean4

theorem toSimpleGraph (c : G.ConnectedComponent) (h : G.IsCycles) : c.toSimpleGraph.spanningCoe.IsCycles :=
  by
  intro v ⟨w, hw⟩
  rw [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph] at hw
  rw [← h ⟨w, hw.2⟩]
  congr 1
  ext w'
  simp only [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph, hw, true_and]

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