coheight_strictAnti

Mathlib.Order.KrullDimension

URI: https://scilib.ai/kg/mathlib#Order.coheight_strictAnti

← MathLib Explorer

English

If y < x and coheight x is finite (coheight x < ⊤), then coheight x < coheight y.

Русский

Если y < x и coheight x < ⊤, то coheight x < coheight y.

LaTeX

$$$ y < x \land (\operatorname{coheight}(x) < \top) \Rightarrow \operatorname{coheight}(x) < \operatorname{coheight}(y) $$$

Lean4

@[gcongr]
theorem coheight_strictAnti {x y : α} (hyx : y < x) (hfin : coheight x < ⊤) : coheight x < coheight y :=
  height_strictMono (α := αᵒᵈ) hyx hfin

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

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

Разделы

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

Аффилиация

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