instIsRefl

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.ReflGen.instIsRefl

English

The generated relation ReflGen r on α is reflexive.

Русский

Сгенерированное relation ReflGen r на α является рефлексивным.

LaTeX

$$$\forall a:\alpha,\; \mathrm{ReflGen}(r)(a,a)$$$

Lean4

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

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

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

Разделы

Аффилиация

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