refl — Mathlib

English

The reflexivity axiom holds: every element is related to itself in the enveloping relation PreEnvelGroupRel.

Русский

Свойство рефлексивности: каждое элемент связано с самим собой в отношении PreEnvelGroupRel.

LaTeX

$$$\forall a:\ PreEnvelGroupRel\, a\ a.$$$

Lean4

@[refl]
theorem refl {R : Type u} [Rack R] {a : PreEnvelGroup R} : PreEnvelGroupRel R a a :=
  PreEnvelGroupRel.rel PreEnvelGroupRel'.refl

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