isSt_trans_real

Mathlib.Analysis.Real.Hyperreal

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

← MathLib Explorer

English

If IsSt r s and IsSt s t, then IsSt r t.

Русский

Если IsSt r s и IsSt s t, то IsSt r t.

LaTeX

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

Lean4

theorem isSt_trans_real {r s t : ℝ} : IsSt r s → IsSt s t → IsSt r t := by
  rw [isSt_real_iff_eq, isSt_real_iff_eq, isSt_real_iff_eq]; exact Eq.trans

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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