isAntisymm

Mathlib.Order.Antichain

URI: https://scilib.ai/kg/mathlib#IsAntichain.isAntisymm

English

If IsAntichain r on the universal set, then r is antisymmetric.

Русский

Если антицепь относительно r на всём множестве, тогда r — антисимметричноe отношение.

LaTeX

$$$IsAntichain(r, \text{univ}) \Rightarrow IsAntisymm(\alpha, r)$$$

Lean4

protected theorem isAntisymm (h : IsAntichain r univ) : IsAntisymm α r :=
  ⟨fun _ _ ha _ => h.eq trivial trivial ha⟩

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

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

Разделы

Аффилиация

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