reflexive_reflGen

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.reflexive_reflGen

English

The relation ReflGen r is reflexive: every element relates to itself.

Русский

Отношение ReflGen r рефлексивно: каждый элемент относится к самому себе.

LaTeX

$$$ \forall x, \mathrm{ReflGen}\ r\ x\ x $$$

Lean4

theorem reflexive_reflGen : Reflexive (ReflGen r) := fun _ ↦ .refl

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

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

Разделы

Аффилиация

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