pairwise_ne — Mathlib

English

From a list l that is Sbtw, one obtains that l is pairwise with respect to inequality: l.Pairwise (≠) holds.

Русский

Из того, что список l удовлетворяет Sbtw, следует, что элементы списка различны попарно: l.Pairwise(≠) выполняется.

LaTeX

$$$\\text{If } l\\text{ is Sbtw, then } l\\text{ is Pairwise }(\\neq).$$$

Lean4

theorem pairwise_ne {l : List P} (h : l.Sbtw R) : l.Pairwise (· ≠ ·) :=
  h.2

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