Henstock — Mathlib

English

Definition: a version of toFilterDistortion with iUnion constraint fixed to π₀.iUnion.

Русский

Определение: вариация toFilterDistortion, фиксирующая iUnion равной π₀.iUnion.

LaTeX

$$$\\text{toFilterDistortioniUnion}(l,I,c,\\pi_0) := \\text{toFilterDistortion}(l,I,c) \\cap \\mathcal{P}\\{\\pi : \\pi.iUnion = \\pi_0.iUnion\\}$$$

Lean4

/-- The `BoxIntegral.IntegrationParams` corresponding to the Henstock-Kurzweil integral. In the
corresponding filter, we require that the tagged partition is subordinate to a (possibly,
discontinuous) positive function `r` and each tag belongs to the corresponding closed box. -/
def Henstock : IntegrationParams :=
  ⟨false, true, false⟩

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