isAntisymm

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

For ordinals, divisibility is antisymmetric: if x ∣ y and y ∣ x, then x = y.

Русский

Для порядков делимость антисимметрична: если x делит y и y делит x, то x = y.

LaTeX

$$$(x \\mid y) \\land (y \\mid x) \\Rightarrow x = y$ for ordinals$$

Lean4

instance isAntisymm : IsAntisymm Ordinal (· ∣ ·) :=
  ⟨@dvd_antisymm⟩

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

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

Разделы

Аффилиация

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