nodup_iff — Mathlib

English

If l is a rotation of l', then l has no duplicates iff l' has no duplicates.

Русский

Если l является вращением l', то у l и l' одно и то же свойство в отношении повторов: либо оба без повторов, либо оба имеют дубликаты.

LaTeX

$$$ l \sim_{\mathrm{rot}} l' \Rightarrow (\text{Nodup}(l) \iff \text{Nodup}(l')) $$$

Lean4

theorem nodup_iff (h : l ~r l') : Nodup l ↔ Nodup l' :=
  h.perm.nodup_iff

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