toFilteriUnion — Mathlib

English

Definition: toFilter l I returns a filter on tagged prepartitions defined via toFilterDistortion and a supremum over c.

Русский

Определение: toFilter l I возвращает фильтр на помеченных пред-разбиениях, задаваемый через toFilterDistortion и супремум по c.

LaTeX

$$$\\text{toFilter}(l,I) := \\big\\lbrace \\text{TaggedPrepartition } \\rbrace$$$

Lean4

/-- A set `s : Set (TaggedPrepartition I)` belongs to `l.toFilteriUnion I π₀` if for any `c : ℝ≥0`
there exists a function `r : ℝⁿ → (0, ∞)` (or a constant `r` if `l.bRiemann = true`) such that `s`
contains each prepartition `π` such that `l.MemBaseSet I c r π` and `π.iUnion = π₀.iUnion`. -/
def toFilteriUnion (I : Box ι) (π₀ : Prepartition I) :=
  ⨆ c : ℝ≥0, l.toFilterDistortioniUnion I c π₀

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