supDegree_single — Mathlib

English

For any a ∈ A and r ∈ R, the supremum degree of the single element (a,r) is either ⊥ if r=0 or D(a) otherwise.

Русский

Для любого a и r верхняя грань степени элемента-одиночки равна ⊥, если r=0, иначе D(a).

LaTeX

$$$\\supDegree D (\\text{single } a r) = \\operatorname{ite}(r=0, ⊥, D(a))$$$

Lean4

theorem supDegree_single (a : A) (r : R) : (single a r).supDegree D = if r = 0 then ⊥ else D a := by
  split_ifs with hr <;> simp [supDegree_single_ne_zero, hr]

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