hasBasis_toFilter — Mathlib

English

The filter (l.toFilter I) has a basis given by l.RCond and the MemBaseSet predicate for π.

Русский

Фильтр (l.toFilter I) имеет базис, задаваемый l.RCond и MemBaseSet для частичных партиций π.

LaTeX

$$$(l.toFilter I).HasBasis (\\\\lambda r. l.RCond (r)) (\\\\lambda r. {\\\\pi | l.MemBaseSet I c (r c) \\\\pi})$$$

Lean4

theorem hasBasis_toFilter (l : IntegrationParams) (I : Box ι) :
    (l.toFilter I).HasBasis (fun r : ℝ≥0 → (ι → ℝ) → Ioi (0 : ℝ) => ∀ c, l.RCond (r c)) fun r =>
      {π | ∃ c, l.MemBaseSet I c (r c) π} :=
  by simpa only [setOf_exists] using hasBasis_iSup (l.hasBasis_toFilterDistortion I)

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