coheight_orderIso

Mathlib.Order.KrullDimension

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

English

If f is an order isomorphism, then coheight(f(x)) = coheight(x) for all x.

Русский

Если f — перестановка порядка, тогда coheight(f(x)) = coheight(x) для каждого x.

LaTeX

$$$ coheight(f(x)) = coheight(x) $$$

Lean4

theorem coheight_orderIso (f : α ≃o β) (x : α) : coheight (f x) = coheight x :=
  height_orderIso (α := αᵒᵈ) f.dual x

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

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

Разделы

Аффилиация

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