infDegree_withTop_some_comp — Mathlib

English

If the support is nonempty, infDegree of the composition with WithTop.some equals WithTop.some of the infDegree.

Русский

Если поддержка непустая, то infDegree композиции с WithTop.some равен WithTop.some от infDegree.

LaTeX

$$$$\operatorname{infDegree}(\operatorname{WithTop.some} \circ D)\, s = \operatorname{WithTop.some}(\operatorname{infDegree}(D)\, s).$$$$

Lean4

theorem infDegree_withTop_some_comp {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
    infDegree (WithTop.some ∘ D) s = infDegree D s :=
  by
  unfold AddMonoidAlgebra.infDegree
  rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]

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