sup — Mathlib

English

If f and g are integrable, then f ⊔ g is integrable.

Русский

Если f и g интегрируемы, то f ⊔ g интегрируемо.

LaTeX

$$$ (Integrable\\ f\\ μ) \\land (Integrable\\ g\\ μ) \\Rightarrow Integrable( f \\sup g )\\ μ $$$

Lean4

@[fun_prop]
theorem sup {β} [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] {f g : α → β}
    (hf : Integrable f μ) (hg : Integrable g μ) : Integrable (f ⊔ g) μ :=
  by
  rw [← memLp_one_iff_integrable] at hf hg ⊢
  exact hf.sup hg

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