α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.250889
ι₂ : Sort ?u.250892
κ : ι → Sort ?u.250897
κ₁ : ι → Sort ?u.250902
κ₂ : ι → Sort ?u.250907
κ' : ι' → Sort ?u.250912
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ (y : β), y ∈ t → ∀ (i : ι), f x y ∈ image2 f (s i) t
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.250889
ι₂ : Sort ?u.250892
κ : ι → Sort ?u.250897
κ₁ : ι → Sort ?u.250902
κ₂ : ι → Sort ?u.250907
κ' : ι' → Sort ?u.250912
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : ι → Set α
t : Set β
⊢ image2 f (⋂ (i : ι), s i) t ⊆ ⋂ (i : ι), image2 f (s i) t
simp_rw [image2_subset_iff, mem_iInter]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.250889
ι₂ : Sort ?u.250892
κ : ι → Sort ?u.250897
κ₁ : ι → Sort ?u.250902
κ₂ : ι → Sort ?u.250907
κ' : ι' → Sort ?u.250912
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ (y : β), y ∈ t → ∀ (i : ι), f x y ∈ image2 f (s i) t
exact fun x hx y hy i => mem_image2_of_mem (hx _) hy