idRel — Mathlib

English

The identity relation is the graph of the identity function: idRel = { p ∈ α×α | p1 = p2 }.

Русский

Идентичное отношение есть график функции тождественного отображения: idRel = { p ∈ α×α | p1 = p2 }.

LaTeX

$$$\\mathrm{idRel} := \\{ p \\in \\alpha \\times \\alpha \\mid p_{1} = p_{2} \\}$$$

Lean4

/-- The identity relation, or the graph of the identity function -/
def idRel {α : Type*} :=
  {p : α × α | p.1 = p.2}

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