subsingleton_reverse_iff — Mathlib

English

Reversing a cycle preserves subsingletonity: s.reverse is subsingleton iff s is subsingleton.

Русский

Обратный цикл сохраняет свойство одиночности: s.reverse — это одиночный цикл тогда и только тогда, когда s — одиночный цикл.

LaTeX

$$$\operatorname{Subsingleton}(s.reverse) \iff \operatorname{Subsingleton}(s)$$$

Lean4

@[simp]
theorem subsingleton_reverse_iff {s : Cycle α} : s.reverse.Subsingleton ↔ s.Subsingleton := by
  simp [length_subsingleton_iff]

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