instIsSymmAntisymmRel

Mathlib.Order.Antisymmetrization

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

English

If r is symmetric, then AntisymmRel r is symmetric as a relation.

Русский

Если r симметричен, то AntisymmRel r симметрично как отношение.

LaTeX

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

Lean4

instance : IsSymm α (AntisymmRel r) where symm _ _ := AntisymmRel.symm

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

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

Разделы

Аффилиация

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