pairwise_disjoint_on_bool — Mathlib

English

For a symmetric relation r on α, Pairwise (r on f) is equivalent to r(f(m), f(n)) for all m < n.

Русский

Для симметричного отношения r на α, Pairwise (r на f) эквивалентно r(f(m), f(n)) для любых m < n.

LaTeX

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

Lean4

theorem pairwise_disjoint_on_bool [PartialOrder α] [OrderBot α] {a b : α} :
    Pairwise (Disjoint on fun c => cond c a b) ↔ Disjoint a b :=
  pairwise_on_bool Disjoint.symm

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