iInf_sets_eq_finite — Mathlib

English

The sets of the infimum of a family of filters indexed by ι equal the union over finite subsets t of ι of the sets of the infimum over t.

Русский

Множества инфимумации семейства фильтров, индексированного ι, равны объединению по конечным подмножествам t индексов ι множеств инфимумации по t.

LaTeX

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

Lean4

theorem iInf_sets_eq_finite {ι : Type*} (f : ι → Filter α) : (⨅ i, f i).sets = ⋃ t : Finset ι, (⨅ i ∈ t, f i).sets :=
  by
  rw [iInf_eq_iInf_finset, iInf_sets_eq]
  exact directed_of_isDirected_le fun _ _ => biInf_mono

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