English
A copy of a continuous open map with a new underlying function equal to the old one yields a map equal to the original when the new function is equal to the old one.
Русский
Копия открытого отображения с новым базовым отображением, равным старому, дает отображение, равное исходному, если новое отображение равно старому.
LaTeX
$$$f' = f \Rightarrow f.copy\, f'\, h = f.$$$
Lean4
/-- Copy of a `ContinuousOpenMap` with a new `ContinuousMap` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : α →CO β) (f' : α → β) (h : f' = f) : α →CO β :=
⟨f.toContinuousMap.copy f' <| h, h.symm.subst f.map_open'⟩
