nontrivial_reverse_iff — Mathlib

English

Reversal preserves nontriviality: s.reverse.Nontrivial ↔ s.Nontrivial.

Русский

Разворот сохраняет не тривиальность: s.reverse не тривиален тогда и только тогда, когда s не тривиален.

LaTeX

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

Lean4

@[simp]
theorem nontrivial_reverse_iff {s : Cycle α} : s.reverse.Nontrivial ↔ s.Nontrivial := by simp [Nontrivial]

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