instLinearOrder

Mathlib.Order.Filter.FilterProduct

URI: https://scilib.ai/kg/mathlib#Filter.Germ.instLinearOrder

← MathLib Explorer

English

If β is a LinearOrder, then Germ β is a LinearOrder.

Русский

Если β — линейный порядок, то Germ β — линейный порядок.

LaTeX

$$$\\text{β is a LinearOrder} \\Rightarrow β^* \\text{ is a LinearOrder}.$$$

Lean4

/-- If `φ` is an ultrafilter then the ultraproduct is a linear order. -/
noncomputable instance instLinearOrder [LinearOrder β] : LinearOrder β* :=
  Lattice.toLinearOrder _

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

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

Разделы

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

Аффилиация

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