instOneCauchy

Mathlib.Algebra.Order.CauSeq.Completion

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

English

The completion has a distinguished one element equal to the image of 1, i.e. 1_{Cauchy abv} = ofRat 1.

Русский

В завершении имеется отмеченная единица, равная образу 1: 1_{Cauchy abv} = ofRat 1.

LaTeX

$$$1_{\mathrm{Cauchy}(abv)} = \operatorname{ofRat}(1)$$$

Lean4

instance : One (Cauchy abv) :=
  ⟨ofRat 1⟩

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

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

Разделы

Аффилиация

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