α : Type u_2
β : Type u_3
γ : Type ?u.11121
δ : Type ?u.11124
ι : Sort u_1
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ Filter.prod (⨅ (i : ι), f i) g = ⨅ (i : ι), Filter.prod (f i) g
α : Type u_2
β : Type u_3
γ : Type ?u.11121
δ : Type ?u.11124
ι : Sort u_1
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ (⨅ (i : ι), f i) ×ˢ g = ⨅ (i : ι), f i ×ˢ g
dsimp only [SProd.sprod]
α : Type u_2
β : Type u_3
γ : Type ?u.11121
δ : Type ?u.11124
ι : Sort u_1
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ (⨅ (x : ι), comap Prod.fst (f x) ⊓ comap Prod.snd g) = ⨅ (i : ι), Filter.prod (f i) g
α : Type u_2
β : Type u_3
γ : Type ?u.11121
δ : Type ?u.11124
ι : Sort u_1
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ Filter.prod (⨅ (i : ι), f i) g = ⨅ (i : ι), Filter.prod (f i) g
rw [Filter.prod, comap_iInf, iInf_inf]
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.11121
δ : Type ?u.11124
ι : Sort u_1
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ (⨅ (x : ι), comap Prod.fst (f x) ⊓ comap Prod.snd g) = ⨅ (i : ι), Filter.prod (f i) g
simp only [Filter.prod, eq_self_iff_true]