ofRat_rat — Mathlib

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

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