α : Type u_2
β : Type u_1
γ : Type ?u.110071
ι : Type ?u.110074
ι' : Sort ?u.110077
inst✝ : Countable β
x : β → Set α
⊢ (⨅ (i : β), 𝓟 (x i)) = generate (range x)
α : Type u_2
β : Type u_1
γ : Type ?u.110071
ι : Type ?u.110074
ι' : Sort ?u.110077
inst✝ : Countable β
x : β → Set α
⊢ IsCountablyGenerated (⨅ (i : β), 𝓟 (x i))
use range x, countable_range x
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.110071
ι : Type ?u.110074
ι' : Sort ?u.110077
inst✝ : Countable β
x : β → Set α
⊢ (⨅ (i : β), 𝓟 (x i)) = generate (range x)
rw [generate_eq_biInf, iInf_range]