English
If e is an OpenPartialHomeomorph between spaces with b in the target, then big-O-with is preserved under composing with e and its inverse: IsBigOWith_C at b is equivalent to IsBigOWith_C at e^{-1}(b) for the composed functions.
Русский
Если e — открытое частичное гомеоморфное отображение между пространствами и b принадлежит целевой области, тогда свойство IsBigOWith сохраняется после композиции с e и его обратной: IsBigOWith_C у b эквивалентно IsBigOWith_C у e^{-1}(b) для композиций функций.
LaTeX
$$$ IsBigOWith C (\\mathcal{N} b) f g \\iff IsBigOWith C (\\mathcal{N} (e^{-1}(b))) (f \\circ e) (g \\circ e) $$$
Lean4
/-- Transfer `IsBigO` over an `OpenPartialHomeomorph`. -/
theorem isBigO_congr (e : OpenPartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} :
f =O[𝓝 b] g ↔ (f ∘ e) =O[𝓝 (e.symm b)] (g ∘ e) :=
by
simp only [IsBigO_def]
exact exists_congr fun C => e.isBigOWith_congr hb
