English
Under suitable directedness, the iInf (infinite infimum) of a directed family of filters has a HasBasis given by indexed intersections.
Русский
При условии направленности, iInf бесконечного минимума семейства фильтров имеет базис, задаваемый пересечениями по индексам.
LaTeX
$$hasBasis_iInf_of_directed (s) (p) (hl) (h) : (iInf i, l i).HasBasis (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd$$
Lean4
theorem hasBasis_iInf_of_directed {ι : Type*} {ι' : Sort _} [Nonempty ι] {l : ι → Filter α} (s : ι → ι' → Set α)
(p : ι → ι' → Prop) (hl : ∀ i, (l i).HasBasis (p i) (s i)) (h : Directed (· ≥ ·) l) :
(⨅ i, l i).HasBasis (fun ii' : ι × ι' => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2 :=
by
refine ⟨fun t => ?_⟩
rw [mem_iInf_of_directed h, Prod.exists]
exact exists_congr fun i => (hl i).mem_iff
