orderTop_smul_not_lt — Mathlib

English

For Hahn series, multiplying by r (a scalar) does not decrease the orderTop of a nonzero series.

Русский

У Hahn-серии умножение на скаляр не уменьшает orderTop ненулевой серии.

LaTeX

$$$$ \text{For } r \in R, x \in \mathrm{HahnSeries}, \; (r \cdot x)_{orderTop} \ge x_{orderTop}. $$$$

Lean4

theorem orderTop_smul_not_lt (r : R) (x : HahnSeries Γ V) : ¬(r • x).orderTop < x.orderTop :=
  by
  by_cases hrx : r • x = 0
  · rw [hrx, orderTop_zero]
    exact not_top_lt
  · simp only [orderTop_of_ne_zero hrx, orderTop_of_ne_zero <| right_ne_zero_of_smul hrx, WithTop.coe_lt_coe]
    exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right (fun _ => r) x.coeff)

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