copy

Mathlib.Order.Copy

URI: https://scilib.ai/kg/mathlib#BoundedOrder.copy

Lean4

/-- A function to create a provable equal copy of a bounded order
with possibly different definitional equalities. -/
def copy {h : LE α} {h' : LE α} (c : @BoundedOrder α h') (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot) (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) :
    @BoundedOrder α h :=
  @BoundedOrder.mk α h (@OrderTop.mk α h { top := top } (fun _ ↦ by simp [eq_top, le_eq]))
    (@OrderBot.mk α h { bot := bot } (fun _ ↦ by simp [eq_bot, le_eq]))

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

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

Разделы

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

Аффилиация

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