reflexive

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#IsRefl.reflexive

English

From IsRefl, we obtain that r is reflexive.

Русский

Из IsRefl следует, что r рефлексивно.

LaTeX

$$$\\text{[IsRefl } \\alpha\\ r] \\Rightarrow \\operatorname{Reflexive}(r)$$$

Lean4

theorem reflexive [IsRefl α r] : Reflexive r := fun x ↦ IsRefl.refl x

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

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

Разделы

Аффилиация

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