toFilteriUnion_congr — Mathlib

English

For given I, c and π0, the filter (l.toFilterDistortioniUnion I c π0) has a basis consisting of the pairs (r, π) where π is a MemBaseSet I c r π and π.iUnion = π0.iUnion.

Русский

Для данных I, c и π0 фильтр (l.toFilterDistortioniUnion I c π0) имеет базис из пар (r, π), где π удовлетворяет MemBaseSet I c r π и π.iUnion = π0.iUnion.

LaTeX

$$$(l.toFilterDistortioniUnion I c π_0).HasBasis \\; l.RCond \\; (\\lambda r. \\{\\pi \\mid l.MemBaseSet I c r \\pi \\land \\pi.iUnion = π_0.iUnion\\})$$$

Lean4

theorem toFilteriUnion_congr (I : Box ι) (l : IntegrationParams) {π₁ π₂ : Prepartition I} (h : π₁.iUnion = π₂.iUnion) :
    l.toFilteriUnion I π₁ = l.toFilteriUnion I π₂ := by simp only [toFilteriUnion, toFilterDistortioniUnion, h]

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