min_orderTop_le_orderTop_sub

Mathlib.RingTheory.HahnSeries.Addition

URI: https://scilib.ai/kg/mathlib#HahnSeries.min_orderTop_le_orderTop_sub

← MathLib Explorer

English

Same as previous: min(x.orderTop, y.orderTop) ≤ (x−y).orderTop.

Русский

То же самое: min(x.orderTop, y.orderTop) ≤ (x−y).orderTop.

LaTeX

$$$$ \min\left( x.orderTop, y.orderTop \right) \le (x - y).orderTop. $$$$

Lean4

theorem min_orderTop_le_orderTop_sub {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} :
    min x.orderTop y.orderTop ≤ (x - y).orderTop :=
  by
  rw [sub_eq_add_neg, ← orderTop_neg (x := y)]
  exact min_orderTop_le_orderTop_add

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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