rotate — Mathlib

English

If c is a circuit, then rotating c by any vertex in its support yields another circuit.

Русский

Если c является петлей (цикл), поворотом вокруг любой вершины из поддержки получаем новую петлю.

LaTeX

$$c.IsCircuit \Rightarrow (c.rotate h).IsCircuit$$

Lean4

protected theorem rotate {u v : V} {c : G.Walk v v} (hc : c.IsCircuit) (h : u ∈ c.support) : (c.rotate h).IsCircuit :=
  by
  refine ⟨hc.isTrail.rotate _, ?_⟩
  cases c
  · exact (hc.ne_nil rfl).elim
  · intro hn
    have hn' := congr_arg length hn
    rw [rotate, length_append, add_comm, ← length_append, take_spec] at hn'
    simp at hn'

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