rank_strictAnti

Mathlib.SetTheory.Ordinal.Rank

URI: https://scilib.ai/kg/mathlib#WellFoundedGT.rank_strictAnti

← MathLib Explorer

English

Under WellFoundedGT, the rank with respect to > is strictly anti-monotone.

Русский

При WellFoundedGT функция ранга по отношению > является строго антитранзитивна.

LaTeX

$$StrictAnti (IsWellFounded.rank (α := α) (\cdot > \cdot))$$

Lean4

theorem rank_strictAnti [Preorder α] [WellFoundedGT α] : StrictAnti (IsWellFounded.rank (α := α) (· > ·)) :=
  fun _ _ a => IsWellFounded.rank_lt_of_rel a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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