height_ne_zero

Mathlib.Order.KrullDimension

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

English

height x ≠ 0 iff x is not minimal.

Русский

height x ≠ 0 эквивалентно тому, что x не минимален.

LaTeX

$$height x ≠ 0 \iff ¬ IsMin x$$

Lean4

theorem height_ne_zero {x : α} : height x ≠ 0 ↔ ¬IsMin x :=
  height_eq_zero.not

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

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

Разделы

Аффилиация

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