isRefl_univ

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.isRefl_univ

English

Set.univ is reflexive with respect to any SetRelIsRefl instance on Set.univ.

Русский

Set.univ является рефлексивным относительно любой инстанции SetRel.IsRefl на Set.univ.

LaTeX

$$Set.univ is reflexive$$

Lean4

instance isRefl_univ : SetRel.IsRefl (.univ : SetRel α α) where refl _ := trivial

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

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

Разделы

Аффилиация

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