re — Mathlib · SciLib

English

Let f be integrable with respect to μ and take values in a complex-like field. Then the real part of f is integrable with respect to μ.

Русский

Пусть f интегрируема по μ и принимает значения в комплексоподобном поле. Тогда вещественная часть f интегрируема по μ.

LaTeX

$$$ \\operatorname{Integrable}(f,\\mu) \\Rightarrow \\operatorname{Integrable}(x \\mapsto \\operatorname{Re}(f(x)),\\mu)$$$

Lean4

@[fun_prop]
theorem re (hf : Integrable f μ) : Integrable (fun x => RCLike.re (f x)) μ :=
  by
  rw [← memLp_one_iff_integrable] at hf ⊢
  exact hf.re

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