McShane — Mathlib

English

Definition: the supremum over c of toFilterDistortioniUnion.

Русский

Определение: сверхгрань по c от toFilterDistortioniUnion.

LaTeX

$$$\\text{toFilteriUnion}(I,\\pi_0) := \\bigvee_{c} \\text{toFilterDistortioniUnion}(I,c,\\pi_0).$$$

Lean4

/-- The `BoxIntegral.IntegrationParams` corresponding to the McShane integral. In the
corresponding filter, we require that the tagged partition is subordinate to a (possibly,
discontinuous) positive function `r`; the tags may be outside of the corresponding closed box
(but still inside the ambient closed box `I.Icc`). -/
def McShane : IntegrationParams :=
  ⟨false, false, false⟩

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