isTheta_completion_right — Mathlib

English

Let f: α → E and g: α → F be functions and l a filter on α. The asymptotic Theta relation between f and the embedding of g into the completion of F is equivalent to the Theta relation between f and g themselves: f =Θ[l] (ĝ) iff f =Θ[l] g.

Русский

Пусть f: α → E и g: α → F — функции, l — фильтр на α. Асимптотическая эквивалентность Θ между f и отображением g в дополнение к F эквивалентна Θ между f и самим g: f =Θ[l] ĝ тогда и только если f =Θ[l] g.

LaTeX

$$$ f =Θ[l]\bigl(\,\hat{g}\bigr) \iff f =Θ[l] g \quad\text{(where }\hat{g}: \alpha \to \widehat{F}\text{ is the canonical embedding).}$$$

Lean4

@[simp, norm_cast]
theorem isTheta_completion_right : f =Θ[l] (fun x ↦ g x : α → F̂) ↔ f =Θ[l] g :=
  and_congr isBigO_completion_right isBigO_completion_left

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