α : Type u_2
β : Type ?u.63130
γ : Type ?u.63133
ι✝ : Sort ?u.63136
ι' : Sort ?u.63139
l l' : Filter α
p : ι✝ → Prop
s✝ : ι✝ → Set α
t : Set α
i : ι✝
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
ι : Type u_1
s : ι → Set α
U : Set α
⊢ (∃ t, U ∈ ⨅ (i : ι) (_ : i ∈ t), 𝓟 (s i)) ↔ ∃ i, Set.Finite i ∧ (⋂ (i_1 : ι) (_ : i_1 ∈ i), s i_1) ⊆ U
α : Type u_2
β : Type ?u.63130
γ : Type ?u.63133
ι✝ : Sort ?u.63136
ι' : Sort ?u.63139
l l' : Filter α
p : ι✝ → Prop
s✝ : ι✝ → Set α
t : Set α
i : ι✝
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
ι : Type u_1
s : ι → Set α
⊢ HasBasis (⨅ (i : ι), 𝓟 (s i)) (fun t => Set.Finite t) fun t => ⋂ (i : ι) (_ : i ∈ t), s i
refine' ⟨fun U => (mem_iInf_finite _).trans _⟩
no goals
α : Type u_2
β : Type ?u.63130
γ : Type ?u.63133
ι✝ : Sort ?u.63136
ι' : Sort ?u.63139
l l' : Filter α
p : ι✝ → Prop
s✝ : ι✝ → Set α
t : Set α
i : ι✝
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
ι : Type u_1
s : ι → Set α
U : Set α
⊢ (∃ t, U ∈ ⨅ (i : ι) (_ : i ∈ t), 𝓟 (s i)) ↔ ∃ i, Set.Finite i ∧ (⋂ (i_1 : ι) (_ : i_1 ∈ i), s i_1) ⊆ U
simp only [iInf_principal_finset, mem_iUnion, mem_principal, exists_prop,
  exists_finite_iff_finset, Finset.set_biInter_coe]