embedRealFun_add — Mathlib

English

The function embedRealFun is additive: embedRealFun(x+y) = embedRealFun(x) + embedRealFun(y).

Русский

Функция embedRealFun является аддитивной: embedRealFun(x+y) = embedRealFun(x) + embedRealFun(y).

LaTeX

$$$\operatorname{embedRealFun}(x+y) = \operatorname{embedRealFun}(x) + \operatorname{embedRealFun}(y)$$$

Lean4

theorem embedRealFun_add (x y : M) : embedRealFun (x + y) = embedRealFun x + embedRealFun y := by
  rw [embedRealFun, ratLt'_add,
    csSup_add (ratLt'_nonempty x) (ratLt'_bddAbove x) (ratLt'_nonempty y) (ratLt'_bddAbove y)]

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