English
If a,b ∈ ℕ∞ and a+b < ⊤, then lift(a+b) h = lift a (ha) + lift b (hb), where ha,hb witness a<⊤, b<⊤ derived from h.
Русский
Если a,b ∈ ℕ∞ и a+b < ⊤, то lift(a+b) h = lift a ha + lift b hb, где ha и hb получены из h как доказательства a<⊤ и b<⊤.
LaTeX
$$$\\\\forall a,b \\\\in \\\\mathbb{N}_{\\\\infty}, \\\\forall h \\\\colon a+b < \\\\top \\\\Rightarrow \\\\operatorname{lift}(a+b)h = \\\\operatorname{lift}(a)(a<\\top) \\\\,+ \\\\operatorname{lift}(b)(b<\\top).$$$
Lean4
@[simp]
theorem lift_add (a b : ℕ∞) (h : a + b < ⊤) : lift (a + b) h = lift a (add_lt_top.1 h).1 + lift b (add_lt_top.1 h).2 :=
by
apply coe_inj.1
simp
