cons — Mathlib

English

If a is not in l and l is nodup, then the list obtained by preprending a is nodup: a :: l has no duplicates whenever a ∉ l and l has no duplicates.

Русский

Если a не принадлежит l и l не содержит повторов, то список a :: l не содержит повторяющихся элементов.

LaTeX

$$$ (a \notin l) \land l.Nodup \rightarrow (a::l).Nodup $$$

Lean4

protected theorem cons (ha : a ∉ l) (hl : Nodup l) : Nodup (a :: l) :=
  nodup_cons.2 ⟨ha, hl⟩

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