ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
⊢ (⋂ (x : ↑I), eval ↑x ⁻¹' s ↑x) ∈ pi f
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
⊢ Set.pi I s ∈ pi f
rw [pi_def, biInter_eq_iInter]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
i : ↑I
⊢ eval ↑i ⁻¹' s ↑i ∈ comap (eval ↑i) (f ↑i)
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
⊢ (⋂ (x : ↑I), eval ↑x ⁻¹' s ↑x) ∈ pi f
refine' mem_iInf_of_iInter hI (fun i => _) Subset.rfl
no goals
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
i : ↑I
⊢ eval ↑i ⁻¹' s ↑i ∈ comap (eval ↑i) (f ↑i)
exact preimage_mem_comap (h i i.2)