English
If c ≠ ⊥ and c ≠ ⊤ in WithBot(WithTop α), and α satisfies AddRightMono and AddRightReflectLE, then a + c ≤ b + c iff a ≤ b.
Русский
Если c ≠ ⊥ и c ≠ ⊤ в WithBot(WithTop α) и α удовлетворяет AddRightMono и AddRightReflectLE, тогда a+c ≤ b+c экв. a ≤ b.
LaTeX
$$$$\\forall a,b,c \\in \\mathrm{WithBot}(\\mathrm{WithTop}(\\alpha)),\\ c \\neq \\bot,\\ c \\neq \\top \\Rightarrow (a+c \\le b+c) \\iff (a \\le b).$$$$
Lean4
@[simp]
protected theorem map_add {F} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithBot α) :
(a + b).map f = a.map f + b.map f := by
induction a
· exact (bot_add _).symm
· induction b
· exact (add_bot _).symm
· rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
rfl
