isAntisymm

Mathlib.Order.Defs.Unbundled

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

English

If r is asymmetric, then r is antisymmetric.

Русский

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

LaTeX

$$$\\\\forall r \\\\ [IsAsymm \\\\alpha \\\\ r], \\\\ IsAntisymm \\\\alpha \\\\ r.$$$

Lean4

protected theorem isAntisymm (r) [IsAsymm α r] : IsAntisymm α r :=
  ⟨fun _ _ h₁ h₂ => (_root_.asymm h₁ h₂).elim⟩

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

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

Разделы

Аффилиация

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