coheight_le_coe_iff

Mathlib.Order.KrullDimension

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

English

Coheight x ≤ n if and only if every y > x has coheight y < n.

Русский

Coheight x ≤ n эквивалентно тому, что для всех y > x выполняется coheight y < n.

LaTeX

$$$ coheight(x) \le n \iff \forall y > x, coheight(y) < n $$$

Lean4

theorem coheight_le_coe_iff {x : α} {n : ℕ} : coheight x ≤ n ↔ ∀ y > x, coheight y < n :=
  height_le_coe_iff (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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