orderTop_single — Mathlib

English

Let a ∈ Γ and r ∈ R with r ≠ 0. Then the Hahn series with a single nonzero term at a and coefficient r has orderTop equal to a.

Русский

Пусть a ∈ Γ и r ∈ R, причём r ≠ 0. Тогда Hahn-серия, имеющая единственный ненулевой член на степени a с коэффициентом r, удовлетворяет orderTop = a.

LaTeX

$$$ (\\mathrm{single}(a,r)).\\mathrm{orderTop} = a \\quad\\text{when } r \\neq 0 $$$

Lean4

@[simp]
theorem orderTop_single (h : r ≠ 0) : (single a r).orderTop = a :=
  (orderTop_of_ne_zero (single_ne_zero h)).trans
    (WithTop.coe_inj.mpr
      (support_single_subset ((single a r).isWF_support.min_mem (support_nonempty_iff.2 (single_ne_zero h)))))

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