untop₀_add — Mathlib

English

For AddZeroClass α, with a,b not top, (a + b).untop₀ = a.untop₀ + b.untop₀.

Русский

Для AddZeroClass α, если a,b не являются ⊤, то (a + b).untop₀ = a.untop₀ + b.untop₀.

LaTeX

$$$[AddZeroClass \alpha] \; ha:\; a \neq \top \; hb:\; b \neq \top \Rightarrow (a + b).untop_0 = a.untop_0 + b.untop_0$$$

Lean4

@[simp]
theorem untop₀_add [AddZeroClass α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    (a + b).untop₀ = a.untop₀ + b.untop₀ :=
  untopD_add ha hb

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