isSt_refl_real

Mathlib.Analysis.Real.Hyperreal

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

English

A real number r is standard with respect to itself: IsSt r r.

Русский

Действительное число r является стандартным по отношению к самому себе: IsSt r r.

LaTeX

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

Lean4

theorem isSt_refl_real (r : ℝ) : IsSt r r :=
  isSt_ofSeq_iff_tendsto.2 tendsto_const_nhds

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

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

Разделы

Аффилиация

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