iInf_sets_eq_finite' — Mathlib

English

A variant of the previous equality with PLift indexing: the sets of the infimum equal the union over Finset of PLifted indices of the infimum.

Русский

Вариант предыдущего равенства с индексами PLift: множества инфимума равны объединению по конечным множествам PLift индексов из ι.

LaTeX

$$$ (\iInf i f_i).sets = \bigcup_{t : Finset (PLift ι)} (\iInf i \in t, f (PLift.down i)).sets $$

Lean4

theorem iInf_sets_eq_finite' (f : ι → Filter α) :
    (⨅ i, f i).sets = ⋃ t : Finset (PLift ι), (⨅ i ∈ t, f (PLift.down i)).sets := by
  rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp, Equiv.plift_apply]

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