untop_orderTop_of_ne_zero — Mathlib

English

If x ≠ 0, then x.orderTop.untop of the appropriate proof equals the minimum of the WF-support.

Русский

Если x ≠ 0, то x.orderTop.untop соответствующим образом равен минимальному элементу WF-поддержки.

LaTeX

$$x ≠ 0 ⇒ x.orderTop.untop (orderTop_ne_top.2 hx) = x.isWF_support.min (support_nonempty_iff.2 hx)$$

Lean4

theorem untop_orderTop_of_ne_zero {x : HahnSeries Γ R} (hx : x ≠ 0) :
    WithTop.untop x.orderTop (orderTop_ne_top.2 hx) = x.isWF_support.min (support_nonempty_iff.2 hx) :=
  WithTop.coe_inj.mp ((WithTop.coe_untop (orderTop x) (orderTop_ne_top.2 hx)).trans (orderTop_of_ne_zero hx))

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