Theorems · Theorem · approximation theory

OpenPartialHomeomorph.isBigOWith_congr

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
  [inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : OpenPartialHomeomorph α β) {b : β},
  b ∈ e.target →
    ∀ {f : β → E} {g : β → F} {C : ℝ},
      Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Transfer IsBigOWith over an OpenPartialHomeomorph.

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

3 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceNormNorm