pairwise_on — Mathlib

English

If r is symmetric, then Pairwise (onFun r f) is equivalent to r(m<n) for all m<n in the index set.

Русский

Если r симметрично, то Pairwise (onFun r f) эквивалентно r(m,n) для всех m<n.

LaTeX

$$$ \text{Pairwise}(\text{onFun } r f) \iff \forall \{m,n\}, m

Lean4

theorem pairwise_on [LinearOrder ι] (hr : Symmetric r) (f : ι → α) :
    Pairwise (r on f) ↔ ∀ ⦃m n⦄, m < n → r (f m) (f n) :=
  ⟨fun h _m _n hmn => h hmn.ne, fun h _m _n hmn => hmn.lt_or_gt.elim (@h _ _) fun h' => hr (h h')⟩

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