isBigOWith_congr — Mathlib

English

A bona fide topological homeomorphism preserves IsBigOWith: IsBigOWith C at b for f,g is equivalent to IsBigOWith C at e^{-1}(b) for the pulled-back functions f∘e, g∘e.

Русский

Гомеоморфизм сохраняет IsBigOWith: IsBigOWith C у b для f,g эквивалентно IsBigOWith C у e^{-1}(b) для функций f∘e и g∘e.

LaTeX

$$$ IsBigOWith C (\\mathcal{N} b) f g \\iff IsBigOWith C (\\mathcal{N} (e^{-1} b)) (f \\circ e) (g \\circ e) $$$

Lean4

/-- Transfer `IsBigOWith` over a `Homeomorph`. -/
theorem isBigOWith_congr (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} {C : ℝ} :
    IsBigOWith C (𝓝 b) f g ↔ IsBigOWith C (𝓝 (e.symm b)) (f ∘ e) (g ∘ e) :=
  e.toOpenPartialHomeomorph.isBigOWith_congr trivial

Похожие утверждения