copy — Mathlib

English

Copying an OrderHom with a new function component yields a new OrderHom with that function and the appropriate proof of monotonicity.

Русский

Копирование OrderHom с новой функцией образует новый OrderHom с этой функцией и соответствующим доказательством монотонности.

LaTeX

$$$\\text{copy}(f,f',h) = \\langle f', h^{\\mathrm{symm}}(f.monotone'), \\rangle$$$

Lean4

/-- Copy of an `OrderHom` 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', h.symm.subst f.monotone'⟩

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