offDiag — Mathlib

English

The off-diagonal of a set s is the set of pairs (a,b) with a,b ∈ s and a ≠ b.

Русский

Вне диагонали множества s — пары (a,b), где a,b ∈ s и a ≠ b.

LaTeX

$$$$\\mathrm{offDiag}(s) = \\{(x,y) \\in s \\times s \\mid x \\neq y\\}\\,.$$$$

Lean4

/-- The off-diagonal of a set `s` is the set of pairs `(a, b)` with `a, b ∈ s` and `a ≠ b`. -/
def offDiag (s : Set α) : Set (α × α) :=
  {x | x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2}

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