circularPreorder

Mathlib.Order.Circular

URI: https://scilib.ai/kg/mathlib#OrderDual.circularPreorder

Lean4

instance circularPreorder (α : Type*) [CircularPreorder α] : CircularPreorder αᵒᵈ :=
  { OrderDual.btw α, OrderDual.sbtw α with
    btw_refl := fun _ => @btw_refl α _ _
    btw_cyclic_left := fun {_ _ _} => @btw_cyclic_right α _ _ _ _
    sbtw_trans_left := fun {_ _ _ _} habc hbdc => hbdc.trans_right habc
    sbtw_iff_btw_not_btw := fun {a b c} => @sbtw_iff_btw_not_btw α _ c b a }

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

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

Разделы

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

Аффилиация

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