instIsReflAntisymmRel

Mathlib.Order.Antisymmetrization

URI: https://scilib.ai/kg/mathlib#instIsReflAntisymmRel

English

If r is reflexive, then AntisymmRel r is reflexive as a relation on α.

Русский

Если r рефлексивен, то AntisymmRel r рефлексивна как отношение на α.

LaTeX

$$$\operatorname{IsRefl}(\alpha, r) \Rightarrow \operatorname{IsRefl}(\alpha, \operatorname{AntisymmRel}(r))$$$

Lean4

instance [IsRefl α r] : IsRefl α (AntisymmRel r) where refl := .refl r

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

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

Разделы

Аффилиация

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