English
A general mechanism to create a provably equal copy of a lattice structure, with prescribed interpretations of the order and lattice operations.
Русский
Обобщенный способ построения копии решетки с заданными интерпретациями порядка и операций
LaTeX
$$$\\exists c' : \\text{Lattice }\\alpha\\;\\text{such that}\\; (c'\\text{ uses specified } le, top, bot, sup, inf)$$$
Lean4
/-- A function to create a provable equal copy of a top order
with possibly different definitional equalities. -/
def copy {h : LE α} {h' : LE α} (c : @OrderTop α h') (top : α) (eq_top : top = (by infer_instance : Top α).top)
(le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderTop α h :=
@OrderTop.mk α h { top := top } fun _ ↦ by simp [eq_top, le_eq]
