nodup — Mathlib

English

If s is subsingleton, then s.Nodup holds.

Русский

Если цикл одиночный, то он является nodup.

LaTeX

$$$\operatorname{Nodup}(s) \text{ given } (\operatorname{Subsingleton}(s))$$$

Lean4

theorem nodup {s : Cycle α} (h : Subsingleton s) : Nodup s :=
  by
  induction s using Quot.inductionOn with
  | _ l
  obtain - | ⟨hd, tl⟩ := l
  · simp
  · have : tl = [] := by simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h
    simp [this]

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