English
If h(x,y) expresses that f(x − y) = f(x) − f(y) and f(⊥) = ⊥, then for all x,y in WithTop α, (x − y).map f = x.map f − y.map f.
Русский
Пусть h выражает тождество f(x − y) = f(x) − f(y) и f(⊥) = ⊥; тогда для любых x,y в WithTop α выполняется (x − y).map f = x.map f − y.map f.
LaTeX
$$$\bigl(\forall x,y\in \alpha\, f(x - y) = f(x) - f(y)\bigr) \land (f(\bot) = \bot) \Rightarrow\forall x,y \in WithTop \alpha,\ (x - y).map f = x.map f - y.map f$$$
Lean4
protected theorem map_sub [Sub β] [Bot β] {f : α → β} (h : ∀ x y, f (x - y) = f x - f y) (h₀ : f ⊥ = ⊥) :
∀ x y : WithTop α, (x - y).map f = x.map f - y.map f
| _, ⊤ => by simp only [sub_top, map_coe, h₀, map_top]
| ⊤, (x : α) => rfl
| (x : α), (y : α) => by simp only [← coe_sub, map_coe, h]
