iInf — Mathlib

English

The corresponding statement for infimum: for almost every x, inf over n of aeSeq hf p n x equals inf over n of f n x.

Русский

Соответствующее утверждение для инфимума: почти для каждого x, inf_n aeSeq hf p n x = inf_n f n x.

LaTeX

$$$ \text{For a.e. } x,\ \inf_n aeSeq\, hf\, p\, n\, x = \inf_n f\, n\, x. $$$

Lean4

theorem iInf [InfSet β] [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ) (hp : ∀ᵐ x ∂μ, p x fun n ↦ f n x) :
    ⨅ n, aeSeq hf p n =ᵐ[μ] ⨅ n, f n :=
  iSup (β := βᵒᵈ) hf hp

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