ofRat_neg — Mathlib

English

For any x in β, the image of its negation is the negation of its image: the embedding preserves subtraction via negation.

Русский

Для любого x ∈ β образ его отрицания равен отрицанию образа: вложение сохраняет вычитание через отрицание.

LaTeX

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

Lean4

theorem ofRat_neg (x : β) : ofRat (-x) = (-ofRat x : Cauchy abv) :=
  congr_arg mk (const_neg _)

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