refl

Mathlib.Order.Comparable

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

English

If r is reflexive, then CompRel r a a holds for every a.

Русский

Если отношение r рефлексивно, то CompRel r a a выполняется для всякого a.

LaTeX

$$$CompRel\,r\,a\,a$$$

Lean4

@[simp, refl]
theorem refl (r : α → α → Prop) [IsRefl α r] (a : α) : CompRel r a a :=
  .of_rel (_root_.refl _)

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

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

Разделы

Аффилиация

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