inf — 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 \\inf g )\\ μ $$$

Lean4

@[fun_prop]
theorem inf {β} [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.inf hg

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