length_nontrivial — Mathlib

English

If a cycle s is nontrivial, then its length is at least 2.

Русский

Если цикл s не тривиален, то его длина не меньше 2.

LaTeX

$$$\operatorname{Nontrivial}(s) \Rightarrow 2 \le \operatorname{length}(s)$$$

Lean4

theorem length_nontrivial {s : Cycle α} (h : Nontrivial s) : 2 ≤ length s :=
  by
  obtain ⟨x, y, hxy, hx, hy⟩ := h
  induction s using Quot.inductionOn with
  | _ l
  rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
  · simp at hx
  · simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy
    simp [hx, hy] at hxy
  · simp [Nat.succ_le_succ_iff]

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