supDegree_eq_of_max — Mathlib

English

Let b be in the image of D. If the inverse image D^{-1}(b) lies in the support of p and every a in supp(p) satisfies D(a) ≤ b, then p.supDegree D = b.

Русский

Пусть b принадлежит диапазону D. Если D^{-1}(b) лежит в опоре p и для каждого a в опоре p выполняется D(a) ≤ b, тогда p.supDegree D = b.

LaTeX

$$$b \in \operatorname{range} D \;\land\; D^{-1}(b) \in \operatorname{supp}(p) \;\land\; \forall a \in \operatorname{supp}(p),\ D(a) \le b \Rightarrow p.supDegree D = b$$$

Lean4

theorem supDegree_eq_of_max {b : B} (hb : b ∈ Set.range D) (hmem : D.invFun b ∈ p.support)
    (hmax : ∀ a ∈ p.support, D a ≤ b) : p.supDegree D = b :=
  sup_eq_of_max hb hmem hmax

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