English
Let (l_i) be a directed family of filters on α, indexed by i ∈ dom, where dom ≠ ∅. Suppose for every i ∈ dom there exist a basis of l_i given by (p_i, s_i). If the family (l_i) is directed under reverse ≤ with respect to GE.ge, then the infimum over i ∈ dom, namely ⨅ i ∈ dom, l_i, has a basis indexed by pairs (i, i′) with i ∈ dom and i′ in the index set corresponding to i, given by the sets s_i i′. In particular, the basic sets of the infimum are precisely the s_i i′, and the indexing reflects the domain condition and the internal basis predicates.
Русский
Пусть {l_i} — направленное семейство фильтров на α, индексируемое i из dom, причём dom непусто. Предположим, что для каждого i в dom существует базис фильтра l_i, заданный парами (p_i, s_i). Если семейство {l_i} направлено относительно порядка обратного включения, тогда биинфинум ⨅_{i∈dom} l_i имеет базис, индексируемый парами (i, i′) с i ∈ dom и i′∈ индексная область для i, заданный наборами s_i i′. Базовые множества биинфима равны s_i i′, а индексация отражает условие домена и соответствующие предикаты базиса.
LaTeX
$$$\\text{HasBasis}\\left(\\bigwedge_{i \\in \\mathrm{dom}} l(i)\\right)\\;\\big(\\lambda ii' : \\Sigma i, ι' i \\mapsto ii'.1 \\in \\mathrm{dom} \\land p(ii'.1, ii'.2)\\big)\\;\\big(\\lambda ii' : \\Sigma i, ι' i \\mapsto s(ii'.1, ii'.2)\\big)$$$$
Lean4
theorem hasBasis_biInf_of_directed' {ι : Type*} {ι' : ι → Sort _} {dom : Set ι} (hdom : dom.Nonempty) {l : ι → Filter α}
(s : ∀ i, ι' i → Set α) (p : ∀ i, ι' i → Prop) (hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i))
(h : DirectedOn (l ⁻¹'o GE.ge) dom) :
(⨅ i ∈ dom, l i).HasBasis (fun ii' : Σ i, ι' i => ii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2 :=
by
refine ⟨fun t => ?_⟩
rw [mem_biInf_of_directed h hdom, Sigma.exists]
refine exists_congr fun i => ⟨?_, ?_⟩
· rintro ⟨hi, hti⟩
rcases (hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩
exact ⟨b, ⟨hi, hb⟩, hbt⟩
· rintro ⟨b, ⟨hi, hb⟩, hibt⟩
exact ⟨hi, (hl i hi).mem_iff.mpr ⟨b, hb, hibt⟩⟩
