Pairwise — Mathlib

English

The pairwise relation on a set s is: for any x,y in s with x ≠ y, r x y.

Русский

Попарность множества s означает: для любых x,y ∈ s, x ≠ y → r(x,y).

LaTeX

$$$\\operatorname{Set.Pairwise}(s,r) :\\Leftrightarrow \\forall x\\in s\\,\\forall y\\in s, x \\neq y \\rightarrow r(x,y)$$$

Lean4

/-- The relation `r` holds pairwise on the set `s` if `r x y` for all *distinct* `x y ∈ s`. -/
protected def Pairwise (s : Set α) (r : α → α → Prop) :=
  ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → r x y

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