pairwise_of_forall_ne — Mathlib

English

If a list has no duplicates and every distinct pair of elements from the list satisfies a relation r, then the list is pairwise with respect to r.

Русский

Если список не содержит повторов и для любых разных элементов a,b из списка выполняется r a b, то список Pairwise r.

LaTeX

$$$ \\operatorname{Nodup}(l) \\land \\big( \\forall a \\in l, \\forall b \\in l, a \\neq b \\rightarrow r\;a\;b \\big) \\Rightarrow \\operatorname{Pairwise} r\\ l. $$$

Lean4

theorem pairwise_of_forall_ne {l : List α} {r : α → α → Prop} (hl : l.Nodup) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) :
    l.Pairwise r := by grind [List.pairwise_iff_forall_sublist]

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