concat — Mathlib

English

If a is not already in l and l has no duplicates, then adding a at the end preserves the no-duplicates property.

Русский

Если a не принадлежит l и в l нет повторов, то добавление a в конец сохраняет свойство отсутствия повторов.

LaTeX

$$$ a \\notin l \\Rightarrow \\operatorname{Nodup}(l) \\Rightarrow \\operatorname{Nodup}(l \\frown [a]). $$$

Lean4

protected theorem concat (h : a ∉ l) (h' : l.Nodup) : (l.concat a).Nodup := by rw [concat_eq_append];
  exact h'.append (nodup_singleton _) (disjoint_singleton.2 h)

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