rel_id_apply₂ — Mathlib

English

For any object X in a RelCat, the relation encoded by the identity morphism is precisely equality: x ~[rel (id X)] y if and only if x = y.

Русский

Для любого объекта X в RelCat отношение, задаваемое идентити-морфизмом, соответствует равенству: x ~[rel (id X)] y тогда же если и только если x = y.

LaTeX

$$$ x \sim_{\mathrm{rel}(\mathrm{id}_X)} y \iff x = y $$$

Lean4

theorem rel_id_apply₂ (x y : X) : x ~[rel (𝟙 X)] y ↔ x = y :=
  .rfl

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