ofRat_add — Mathlib

English

Let x and y be elements of β. The embedding of β into the Cauchy completion (with respect to the absolute value abv) preserves addition: the image of x + y is the sum of the images of x and y.

Русский

Пусть x, y ∈ β. Встраивание β в дополнение Коши относительно абсалютного значения abv сохраняет сложение: образ x + y равен сумме образов x и y.

LaTeX

$$$\operatorname{ofRat}(x+y) = (\operatorname{ofRat}x + \operatorname{ofRat}y : \mathrm{CauSeq.Completion.Cauchy}\,abv)$$$

Lean4

theorem ofRat_add (x y : β) : ofRat (x + y) = (ofRat x + ofRat y : Cauchy abv) :=
  congr_arg mk (const_add _ _)

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