α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (↑(Homeomorph.symm e) b)) (f ∘ ↑e) (g ∘ ↑e)
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ f =o[𝓝 b] g ↔ (f ∘ ↑e) =o[𝓝 (↑(Homeomorph.symm e) b)] (g ∘ ↑e)
simp only [IsLittleO_def]
no goals
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (↑(Homeomorph.symm e) b)) (f ∘ ↑e) (g ∘ ↑e)
exact forall₂_congr fun c _hc => e.isBigOWith_congr