English
For any q ∈ ℚ, its image in the Cauchy completion via ofRat is exactly its canonical cast in the completion; i.e. ofRat(q) equals q cast into CauSeq.Completion.Cauchy abs.
Русский
Для любого q ∈ ℚ образ в дополнении Коши через ofRat совпадает с каноническим представлением в дополнении; ofRat(q) = q.cast.
LaTeX
$$$\operatorname{ofRat}(q) = (q : \mathrm{CauSeq.Completion.Cauchy}(\lvert \cdot \lvert)).$$$
Lean4
@[simp]
theorem ofRat_rat {abv : ℚ → ℚ} [IsAbsoluteValue abv] (q : ℚ) : ofRat (q : ℚ) = (q : Cauchy abv) :=
rfl