instLinearOrder

Mathlib.Analysis.Real.Hyperreal

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

Lean4

noncomputable instance : LinearOrder ℝ* :=
  inferInstanceAs (LinearOrder (Germ _ _))

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

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

Разделы

Аффилиация

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