English
Copy of a lattice homomorphism with a new underlying map; preserves all lattice homomorphism structure with the new map.
Русский
Копия гомоморфизма решетки с новой базовой функцией; сохраняет всю структуру, соответствующую новой функции.
LaTeX
$$$\mathrm{copy}\ f\ f'\ h : \mathrm{LatticeHom}(\\alpha,\\beta)$, with underlying function equal to f' and equality h.$$
Lean4
/-- Copy of a `LatticeHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : LatticeHom α β) (f' : α → β) (h : f' = f) : LatticeHom α β :=
{ f.toSupHom.copy f' h, f.toInfHom.copy f' h with }
