English
For a directed family f_i, the sets of the infimum equal the union of the sets: (iInf f).sets = ⋃ i (f_i).sets.
Русский
Для направленного семейства фильтров f_i множества наименьшего верхнего предела равны объединению множеств: (iInf f).sets = ⋃ i (f_i).sets.
LaTeX
$$ (iInf f).sets = ⋃ i, (f i).sets$$
Lean4
theorem iInf_sets_eq {f : ι → Filter α} (h : Directed (· ≥ ·) f) [ne : Nonempty ι] : (iInf f).sets = ⋃ i, (f i).sets :=
let ⟨i⟩ := ne
let u :=
{ sets := ⋃ i, (f i).sets
univ_sets := mem_iUnion.2 ⟨i, univ_mem⟩
sets_of_superset := by
simp only [mem_iUnion, exists_imp]
exact fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩
inter_sets := by
simp only [mem_iUnion, exists_imp]
intro x y a hx b hy
rcases h a b with ⟨c, ha, hb⟩
exact ⟨c, inter_mem (ha hx) (hb hy)⟩ }
have : u = iInf f := eq_iInf_of_mem_iff_exists_mem mem_iUnion
congr_arg Filter.sets this.symm
