English
Let f: α →+*o β be an ordered ring homomorphism and f': α → β a function with h: f' = f. Then the copy f.copy f' h is exactly f.
Русский
Пусть f: α →+*o β — упорядоченный кольцевой гомоморфизм и f': α → β — произвольная функция с h: f' = f. Тогда копия f: f.copy f' h равна самому f.
LaTeX
$$$\forall f:\alpha \to+*o\beta,\; \forall f':\alpha \to\beta,\; \forall h:\, f' = f,\; f.copy f' h = f$$$
Lean4
/-- Copy of an `OrderRingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : α →+*o β) (f' : α → β) (h : f' = f) : α →+*o β :=
{ f.toRingHom.copy f' h, f.toOrderAddMonoidHom.copy f' h with }
