hasBasis_toFilterDistortioniUnion

English

For l, I, c the filter (l.toFilterDistortion I c) has a basis given by l.RCond and the MemBaseSet predicate.

Русский

Для l, I, c фильтр (l.toFilterDistortion I c) имеет базис, задаваемый l.RCond и MemBaseSet.

LaTeX

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

Lean4

theorem hasBasis_toFilterDistortioniUnion (l : IntegrationParams) (I : Box ι) (c : ℝ≥0) (π₀ : Prepartition I) :
    (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion} :=
  (l.hasBasis_toFilterDistortion I c).inf_principal _

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