nontrivial_iff — Mathlib

English

If s is nodup then Nontrivial s ↔ ¬ Subsingleton s.

Русский

Если s без повторов, то не тривиальность эквивалентна не-одиночности.

LaTeX

$$$\operatorname{Nodup}(s) \Rightarrow (\operatorname{Nontrivial}(s) \iff \neg \operatorname{Subsingleton}(s))$$$

Lean4

theorem nontrivial_iff {s : Cycle α} (h : Nodup s) : Nontrivial s ↔ ¬Subsingleton s :=
  by
  rw [length_subsingleton_iff]
  induction s using Quotient.inductionOn'
  simp only [mk''_eq_coe, nodup_coe_iff] at h
  simp [h, Nat.succ_le_iff]

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