Riemann — Mathlib

English

Equivalently define toFilterDistortion as the intersection of a family of principal filters generated by MemBaseSet.

Русский

Алтернативное определение toFilterDistortion как пересечение семейства главных фильтров, порождаемых MemBaseSet.

LaTeX

$$$\\text{toFilterDistortion}(l,I,c) = \\bigcap_{\\pi: MemBaseSet I c r \\pi} \\mathbf{P}(\\pi)$$$

Lean4

/-- The `BoxIntegral.IntegrationParams` corresponding to the Riemann integral. In the
corresponding filter, we require that the diameters of all boxes `J` of a tagged partition are
bounded from above by a constant upper estimate that may not depend on the geometry of `J`, and each
tag belongs to the corresponding closed box. -/
def Riemann : IntegrationParams where
  bRiemann := true
  bHenstock := true
  bDistortion := false

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