ι : Sort u_2
α : Type u_1
β : Type ?u.5424
X : Type ?u.5427
Y : Type ?u.5430
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (Filter.lift' l (Iic ∘ 𝓟)) p fun i => Iic (𝓟 (s i))
ι : Sort u_2
α : Type u_1
β : Type ?u.5424
X : Type ?u.5427
Y : Type ?u.5430
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (𝓝 l) p fun i => Iic (𝓟 (s i))
rw [nhds_eq]
no goals
ι : Sort u_2
α : Type u_1
β : Type ?u.5424
X : Type ?u.5427
Y : Type ?u.5430
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (Filter.lift' l (Iic ∘ 𝓟)) p fun i => Iic (𝓟 (s i))
exact h.lift' monotone_principal.Iic