ofCauchy_add

Mathlib.Data.Real.Basic

URI: https://scilib.ai/kg/mathlib#Real.ofCauchy_add

English

The embedding preserves addition: the image of a + b equals the sum of the images.

Русский

Встраивание сохраняет сложение: образ a + b равен сумме образов.

LaTeX

$$$$\operatorname{ofCauchy}(a+b) = \operatorname{ofCauchy}(a) + \operatorname{ofCauchy}(b).$$$$

Lean4

theorem ofCauchy_add (a b) : (⟨a + b⟩ : ℝ) = ⟨a⟩ + ⟨b⟩ :=
  (add_def _ _).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru