isTheta_completion_left — Mathlib

English

The Theta relation to the completion space corresponds to Theta in the base space on the left.

Русский

Отношение Θ между функциями в пространстве дополнения соответствует Θ в базовом пространстве слева.

LaTeX

$$$ (fun x \mapsto g x : α \to F̂) =Θ[l] f \;\iff\; g =Θ[l] f$$

Lean4

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

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