pairwise_disjoint_on — Mathlib

English

In a partial order with bottom, and index type ι, Pairwise (Disjoint on f) is equivalent to Disjoint (f m) and (f n) whenever m < n.

Русский

В частичном порядке с нулём и индексом ι, Pairwise (Disjoint on f) эквивалентно Disjoint(f(m), f(n)) при m < n.

LaTeX

$$$ \text{Pairwise}(\operatorname{Disjoint} \circ f) \iff \forall m,n, m

Lean4

theorem pairwise_disjoint_on [PartialOrder α] [OrderBot α] [LinearOrder ι] (f : ι → α) :
    Pairwise (Disjoint on f) ↔ ∀ ⦃m n⦄, m < n → Disjoint (f m) (f n) :=
  Symmetric.pairwise_on Disjoint.symm f

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