offDiag — Mathlib

English

Let S be a finite set. The off-diagonal of S is the set of ordered pairs (a,b) with a,b ∈ S and a ≠ b.

Русский

Пусть S — конечное множество. Вне диагонали S — множество упорядоченных пар (a,b) таких, что a,b ∈ S и a ≠ b.

LaTeX

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

Lean4

/-- Given a finite set `s`, the off-diagonal, `s.offDiag` is the set of pairs `(a, b)` with `a ≠ b`
for `a, b ∈ s`. -/
def offDiag :=
  (s ×ˢ s).filter fun a : α × α => a.fst ≠ a.snd

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