isTheta_ofReal_left — Mathlib

English

Let f: α → ℝ and g: α → E. Then (f · : α → ℂ) =Θ[l] g iff f =Θ[l] g; i.e., the Theta relation is preserved by embedding a real-valued map into complex-valued form.

Русский

Пусть f: α → ℝ и g: α → E. Тогда (f через вложение в ℂ) =Θ[l] g эквивалентно f =Θ[l] g; т. е. отношение Θ сохраняется при вложении Real в Complex.

LaTeX

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

Lean4

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

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