α : Type u_1
β : Type ?u.169
ι : Sort ?u.172
l l' la : Filter α
lb : Filter β
f : Filter α
⊢ Filter.lift' f powerset = ⨅ (b : Set α) (_ : b ∈ f.sets), 𝓟 (𝒫 b)
α : Type u_1
β : Type ?u.169
ι : Sort ?u.172
l l' la : Filter α
lb : Filter β
f : Filter α
⊢ smallSets f = generate (powerset '' f.sets)
simp_rw [generate_eq_biInf, smallSets, iInf_image]
no goals
α : Type u_1
β : Type ?u.169
ι : Sort ?u.172
l l' la : Filter α
lb : Filter β
f : Filter α
⊢ Filter.lift' f powerset = ⨅ (b : Set α) (_ : b ∈ f.sets), 𝓟 (𝒫 b)
rfl