ι : Sort u_2
α : Type u_1
β : Type ?u.9675
X : Type ?u.9678
Y : Type ?u.9681
f : ι → Filter α
⊢ Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟) = ⨅ (i : ι), Filter.lift' (f i) (Iic ∘ 𝓟)
ι : Sort u_2
α : Type u_1
β : Type ?u.9675
X : Type ?u.9678
Y : Type ?u.9681
f : ι → Filter α
⊢ 𝓝 (⨅ (i : ι), f i) = ⨅ (i : ι), 𝓝 (f i)
simp only [nhds_eq]
no goals
ι : Sort u_2
α : Type u_1
β : Type ?u.9675
X : Type ?u.9678
Y : Type ?u.9681
f : ι → Filter α
⊢ Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟) = ⨅ (i : ι), Filter.lift' (f i) (Iic ∘ 𝓟)
apply lift'_iInf_of_map_univ <;> simp