pairwise_of_set_pairwise — Mathlib

English

If l is a nodup list and the set of its elements is pairwise with respect to r, then the list l is pairwise with respect to r.

Русский

Если список l без повторов, и множество элементов l попарно удовлетворяет отношению r, то и сам список l попарно удовлетворяет r.

LaTeX

$$$l\\text{ nodup} \land \\{x\\mid x\\in l\\} \\text{ Pairwise } r \\Rightarrow l \\text{ Pairwise } r$$$

Lean4

theorem pairwise_of_set_pairwise {l : List α} {r : α → α → Prop} (hl : l.Nodup) (h : {x | x ∈ l}.Pairwise r) :
    l.Pairwise r :=
  hl.pairwise_of_forall_ne h

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