toFilterDistortion — Mathlib

English

If l1 ≤ l2 and c1 ≤ c2 and r1 ≤ r2 componentwise, then MemBaseSet is preserved across π.

Русский

Если l1 ≤ l2 и c1 ≤ c2 и r1 ≤ r2 по компонентам, MemBaseSet сохраняется.

LaTeX

$$$l_1 \\le l_2 \\ \u2200 c_1 \\le c_2 \\ \u2026 \\Rightarrow l_2.MemBaseSet I c_2 r_2 \\pi$$$

Lean4

/-- A set `s : Set (TaggedPrepartition I)` belongs to `l.toFilterDistortion I c` if 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 π`. -/
def toFilterDistortion (l : IntegrationParams) (I : Box ι) (c : ℝ≥0) : Filter (TaggedPrepartition I) :=
  ⨅ (r : (ι → ℝ) → Ioi (0 : ℝ)) (_ : l.RCond r), 𝓟 {π | l.MemBaseSet I c r π}

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