English
If e is an open partial homeomorphism with b in its target, then IsBigOWith C at b for f, g is equivalent to IsBigOWith C at e^{-1}b for f ∘ e and g ∘ e.
Русский
Если e является отображением между множествами с открытым частичным гомоморфизмом и b лежит в его мишени, то IsBigOWith C в точке b для функций f, g эквивалентно IsBigOWith C в точке e^{-1}b для функций f ∘ e и g ∘ e.
LaTeX
$$$$ IsBigOWith C (\\nhds b)\\ f\\ g \\iff IsBigOWith C (\\nhds (e.symm.b))\\ (f \\circ e) (g \\circ e) $$$$
Lean4
/-- Transfer `IsBigOWith` over an `OpenPartialHomeomorph`. -/
theorem isBigOWith_congr (e : OpenPartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} {C : ℝ} :
IsBigOWith C (𝓝 b) f g ↔ IsBigOWith C (𝓝 (e.symm b)) (f ∘ e) (g ∘ e) :=
⟨fun h =>
h.comp_tendsto <| by
have := e.continuousAt (e.map_target hb)
rwa [ContinuousAt, e.rightInvOn hb] at this,
fun h =>
(h.comp_tendsto (e.continuousAt_symm hb)).congr' rfl
((e.eventually_right_inverse hb).mono fun _ hx => congr_arg f hx)
((e.eventually_right_inverse hb).mono fun _ hx => congr_arg g hx)⟩
