lt_def

Mathlib.Order.Filter.FilterProduct

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

English

The order on germs is the LiftRel of the base order: <β^*> equals LiftRel (<β).

Русский

Порядок в Гермах равен LiftRel базового порядка: <β^*> = LiftRel(<β).

LaTeX

$$$<_{β^*} = \\mathrm{LiftRel}(<).$$$

Lean4

theorem lt_def [Preorder β] : ((· < ·) : β* → β* → Prop) = LiftRel (· < ·) :=
  by
  ext ⟨f⟩ ⟨g⟩
  exact coe_lt

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

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

Разделы

Аффилиация

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