diagonal — Mathlib

English

The diagonal α is the subset of α × α consisting of all pairs (a,a).

Русский

Диагональ множества α — подмножество α × α, состоящее из пар вида (a,a).

LaTeX

$$$$\\mathrm{diagonal}(\\alpha) = \\{(x,y) \\in \\alpha \\times \\alpha \\mid x = y\\}. $$$$

Lean4

/-- `diagonal α` is the set of `α × α` consisting of all pairs of the form `(a, a)`. -/
def diagonal (α : Type*) : Set (α × α) :=
  {p | p.1 = p.2}

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