copy

Mathlib.Order.Copy

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

Lean4

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

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

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

Разделы

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

Аффилиация

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