isAsymm

Mathlib.Data.List.Shortlex

URI: https://scilib.ai/kg/mathlib#List.Shortlex.isAsymm

English

If r is asymmetric, then the induced Shortlex order on List α is asymmetric.

Русский

Если r ассиметрично, тогда на списках порядок Shortlex ассиметричен.

LaTeX

$$$ [IsAsymm\\ α\\ r] \\Rightarrow IsAsymm (List \\alpha) (Shortlex r). $$$

Lean4

instance isAsymm [IsAsymm α r] : IsAsymm (List α) (Shortlex r) :=
  inferInstanceAs <| IsAsymm (List α) (InvImage _ _)

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

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

Разделы

Аффилиация

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