supDegree_withBot_some_comp — Mathlib

English

If a is in the support and is a maximal point with respect to D on the support, then supDegree D p equals D a.

Русский

Если a принадлежит поддержке p и является максимумом по D на поддержке, то supDegree D p = D a.

LaTeX

$$$\\text{If } a \\in p\\!\\text{support} \\land IsMaxOn(D, p\\!\\text{support}, a) \\Rightarrow p\\!\\sup(D)=D(a)$$$

Lean4

theorem supDegree_withBot_some_comp {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
    supDegree (WithBot.some ∘ D) s = supDegree D s :=
  by
  unfold AddMonoidAlgebra.supDegree
  rw [← Finset.coe_sup' hs, Finset.sup'_eq_sup]

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