reverse_eq_single — Mathlib

English

For any n and i, c.reverse equals single n h iff c equals single n h.

Русский

Для любых n и h утверждается: c.reverse = single n h тогда и только тогда, когда c = single n h.

LaTeX

$$$\\forall {n} {hn},\\ {c:\\mathrm{Composition}(n)},\\ c.reverse = \\mathrm{single}\\;n\\;hn \\iff c = \\mathrm{single}\\;n\\;hn$$$

Lean4

@[simp]
theorem reverse_eq_single {hn : 0 < n} {c : Composition n} : c.reverse = single n hn ↔ c = single n hn :=
  reverse_injective.eq_iff' <| reverse_single _

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