rank_strictMono

Mathlib.SetTheory.Ordinal.Rank

URI: https://scilib.ai/kg/mathlib#WellFoundedLT.rank_strictMono

← MathLib Explorer

English

If a < b in a preorder with WellFoundedLT, then rank(a) < rank(b).

Русский

Если a < b в пределе с WellFoundedLT, то rank(a) < rank(b).

LaTeX

$$StrictMono (IsWellFounded.rank (α := α) (\cdot < \cdot))$$

Lean4

theorem rank_strictMono [Preorder α] [WellFoundedLT α] : StrictMono (IsWellFounded.rank (α := α) (· < ·)) := fun _ _ =>
  IsWellFounded.rank_lt_of_rel

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

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

Разделы

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

Аффилиация

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