orderTop_eq_of_le — Mathlib

English

If g ∈ x.support and g ≤ g' for all g' ∈ x.support, then orderTop x = g.

Русский

Если g принадлежит поддержке x и g ≤ g' для всех g' в поддержке, тогда orderTop x = g.

LaTeX

$$orderTop x = g, если g ∈ x.support и ∀ g' ∈ x.support, g ≤ g'$$

Lean4

theorem orderTop_eq_of_le {x : HahnSeries Γ R} {g : Γ} (hg : g ∈ x.support) (hx : ∀ g' ∈ x.support, g ≤ g') :
    orderTop x = g := by
  rw [orderTop_of_ne_zero <| support_nonempty_iff.mp <| Set.nonempty_of_mem hg, x.isWF_support.min_eq_of_le hg hx]

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