isTheta_ofReal_right — Mathlib

English

Let f: α → E and g: α → ℝ. Then f =Θ[l] (g · : α → ℂ) iff f =Θ[l] g; i.e., the Theta relation is preserved when viewing g as a complex-valued function.

Русский

Пусть f: α → E и g: α → ℝ. Тогда f =Θ[l] (g · : α → ℂ) эквивалентно f =Θ[l] g.

LaTeX

$$$ f =Θ[l] (g \\cdot : \\alpha \\to \\mathbb{C}) \\leftrightarrow f =Θ[l] g $$$

Lean4

@[simp, norm_cast]
theorem isTheta_ofReal_right {f : α → E} {g : α → ℝ} : f =Θ[l] (g · : α → ℂ) ↔ f =Θ[l] g :=
  (isTheta_ofReal g l).isTheta_congr_right

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