English
If l has a basis {b_i} indexed by i in ι and x belongs to blimsup u l p, then there is a parametrization f with values in the basis such that x ∈ u(f(i)) and p(f(i)) and f(i) ∈ b i for each i.
Русский
Пусть l имеет базис {b_i}. Если x ∈ blimsup u l p, то существует отображение f с f(i) ∈ β such that x ∈ u(f(i)) и p(f(i)) и f(i) ∈ b i.
LaTeX
$$∃ f : {i | q i} → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i$$
Lean4
theorem exists_forall_mem_of_hasBasis_mem_blimsup {l : Filter β} {b : ι → Set β} {q : ι → Prop} (hl : l.HasBasis q b)
{u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ blimsup u l p) :
∃ f : {i | q i} → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i :=
by
rw [blimsup_eq_iInf_biSup] at hx
simp only [iSup_eq_iUnion, iInf_eq_iInter, mem_iInter, mem_iUnion, exists_prop] at hx
choose g hg hg' using hx
refine ⟨fun i : {i | q i} => g (b i) (hl.mem_of_mem i.2), fun i => ⟨?_, ?_⟩⟩
· exact hg' (b i) (hl.mem_of_mem i.2)
· exact hg (b i) (hl.mem_of_mem i.2)
