English
Let dom be a nonempty set and l: dom → Filter α be a directed family under GE.ge for which each l(i) has a basis (p(i), s(i)) indexed by i′. Then the infimum ⨅ i ∈ dom, l(i) has a basis indexed by pairs (i, i′) with the basic sets s(i)(i′) and predicates p(i)(i′).
Русский
Пусть dom не пусто и имеется направленное семейство фильтров l(i) (i ∈ dom). Пусть для каждого i существует базис (p(i), s(i)) индексируемый i′. Тогда биинфинум ⨅_{i∈dom} l(i) имеет базис, индексируемый парами (i, i′), с базисными множествами s(i)(i′) и предикатами p(i)(i′).
LaTeX
$$$\\text{HasBasis}\\left(\\bigwedge_{i} l(i)\\right)\\left(\\lambda ii' : \\Sigma i, ι' i \\mapsto ii'.1 \\in dom \\land p(ii'.1, ii'.2)\\right)\\left(\\lambda ii' : \\Sigma i, ι' i \\mapsto s(ii'.1, ii'.2)\\right)$$$
Lean4
theorem hasBasis_biInf_of_directed {ι : Type*} {ι' : Sort _} {dom : Set ι} (hdom : dom.Nonempty) {l : ι → Filter α}
(s : ι → ι' → Set α) (p : ι → ι' → 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' : ι × ι' => 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, Prod.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⟩⟩
