English
Let α be a field with a map inducedMap: α → β. Then the induced map preserves addition: for all x,y ∈ α, inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y.
Русский
Пусть существует индуцированное отображение α→β. Тогда индуцированная карта сохраняет сложение: для любых x,y ∈ α выполняется inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y.
LaTeX
$$$ \forall x,y \in \alpha,\; \operatorname{inducedMap} \alpha \beta (x+y) = \operatorname{inducedMap} \alpha \beta x + \operatorname{inducedMap} \alpha \beta y $$$
Lean4
theorem inducedMap_add (x y : α) : inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y :=
by
rw [inducedMap, cutMap_add]
exact csSup_add (cutMap_nonempty β x) (cutMap_bddAbove β x) (cutMap_nonempty β y) (cutMap_bddAbove β y)
