height_le_height

Mathlib.Order.KrullDimension

URI: https://scilib.ai/kg/mathlib#GCongr.height_le_height

English

Given a ≤ b, height a ≤ height b.

Русский

Пусть a ≤ b. Тогда height a ≤ height b.

LaTeX

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

Lean4

@[gcongr]
protected theorem _root_.GCongr.height_le_height (a b : α) (hab : a ≤ b) : height a ≤ height b :=
  height_mono hab

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

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

Разделы

Аффилиация

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