eq_of_isSt_real

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.eq_of_isSt_real

English

If IsSt r s holds for real r and s, then r = s.

Русский

Если IsSt r s выполняется для вещественных r и s, тогда r = s.

LaTeX

$$$\forall r,s \in \mathbb{R}, \ \mathrm{IsSt}(r,s) \rightarrow r = s$$$

Lean4

theorem eq_of_isSt_real {r s : ℝ} : IsSt r s → r = s :=
  (isSt_refl_real r).unique

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

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

Разделы

Аффилиация

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