instIsReflReflTransGen

Mathlib.Logic.Relation

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

English

The type ReflTransGen r is equipped with reflexivity.

Русский

У типа ReflTransGen r присутствует рефлексивность.

LaTeX

$$$$\\text{IsRefl }\\alpha (\\operatorname{ReflTransGen} r)$$$$

Lean4

instance : IsRefl α (ReflTransGen r) :=
  ⟨@ReflTransGen.refl α r⟩

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

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

Разделы

Аффилиация

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