ofRat_nnratCast

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.ofRat_nnratCast

English

Two canonical casts from NNRat and Rat into CauSeq.Completion.Cauchy abv coincide with the ofRat embedding.

Русский

Сопоставления nnratCast и ratCast совпадают с вложением ofRat.

LaTeX

$$nnratCast and ratCast are compatible with ofRat: $$\text{ofRat} = \text{nnratCast} \text{ and } \text{ratCast}$$$$

Lean4

@[simp, norm_cast]
theorem ofRat_nnratCast (q : ℚ≥0) : ofRat (q : β) = (q : Cauchy abv) :=
  rfl

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

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

Разделы

Аффилиация

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