reflGen_eq_self

Mathlib.Logic.Relation

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

English

If r is reflexive, then the reflexive-transitive closure ReflGen r equals r.

Русский

Если r рефлексивно, то ReflGen r равняется r.

LaTeX

$$$ \forall {α} {r : α \to α \to \mathrm{Prop}}, \mathrm{Reflexive}\ r \to \mathrm{ReflGen}\ r = r $$$

Lean4

theorem reflGen_eq_self (hr : Reflexive r) : ReflGen r = r :=
  by
  ext x y
  simpa only [reflGen_iff, or_iff_right_iff_imp] using fun h ↦ h ▸ hr y

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

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

Разделы

Аффилиация

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