reflexive_reflTransGen

Mathlib.Logic.Relation

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

English

For any relation r, the closure ReflTransGen r is reflexive.

Русский

Для любого отношения r замыкание ReflTransGen r является рефлексивным.

LaTeX

$$$$\\text{Theorem: } \\text{ReflTransGen } r \\text{ is Reflexive},$$$$

Lean4

theorem reflexive_reflTransGen : Reflexive (ReflTransGen r) := fun _ ↦ refl

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

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

Разделы

Аффилиация

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