coheight_anti

Mathlib.Order.KrullDimension

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

English

Coheight is antitone: if a ≤ b then coheight(a) ≥ coheight(b).

Русский

Ко‑высота анти‑монотонна: если a ≤ b, то coheight(a) ≥ coheight(b).

LaTeX

$$$\forall a,b:\alpha,\ a \le b \Rightarrow \operatorname{coheight}(a) \ge \operatorname{coheight}(b).$$$

Lean4

theorem coheight_anti : Antitone (α := α) coheight :=
  (height_mono (α := αᵒᵈ)).dual_left

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

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

Разделы

Аффилиация

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