refl

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.refl

English

If R is reflexive, then every element is related to itself: a ~_R a for all a.

Русский

Если R рефлексивно, то для каждого элемента выполняется a ~_R a.

LaTeX

$$a \sim_R a$$

Lean4

protected theorem refl [R.IsRefl] (a : α) : a ~[R] a :=
  refl_of (· ~[R] ·) a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru