English
Copy of a bounded lattice homomorphism with a new underlying function, preserving equality with the original when the new function equals the old one.
Русский
Копия гомоморфизма ограниченной решетки с новой базовой функцией, сохраняющая эквивалентность исходному при равенстве функций.
LaTeX
$$$\\text{BoundedLatticeHom.copy}(f,f',h)\\ is\\ a\\ boundedLatticeHom\\;\\text{and}\\;h:\\ f' = f$$$
Lean4
/-- Copy of a `BoundedLatticeHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = f) : BoundedLatticeHom α β :=
{ f.toLatticeHom.copy f' h, f.toBoundedOrderHom.copy f' h with }
