ext_cauchy

Mathlib.Data.Real.Basic

URI: https://scilib.ai/kg/mathlib#Real.ext_cauchy

English

If two real numbers have equal Cauchy representations, then the numbers are equal.

Русский

Если два вещественных числа имеют одинаковые представления как пределы Коши, то сами числа равны.

LaTeX

$$$$x.cauchy = y.cauchy \Rightarrow x = y.$$$$

Lean4

theorem ext_cauchy {x y : Real} : x.cauchy = y.cauchy → x = y :=
  ext_cauchy_iff.2

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

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

Разделы

Аффилиация

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