α : Type u_1
β : Type u_2
γ : Type ?u.185546
ι : Sort ?u.185549
ι' : Sort ?u.185552
ι₂ : Sort ?u.185555
κ : ι → Sort ?u.185560
κ₁ : ι → Sort ?u.185565
κ₂ : ι → Sort ?u.185570
κ' : ι' → Sort ?u.185575
S : Set (Set α)
f : α → β
⊢ (f '' ⋂ (i : Set α) (_ : i ∈ S), i) ⊆ ⋂ (s : Set α) (_ : s ∈ S), f '' s
α : Type u_1
β : Type u_2
γ : Type ?u.185546
ι : Sort ?u.185549
ι' : Sort ?u.185552
ι₂ : Sort ?u.185555
κ : ι → Sort ?u.185560
κ₁ : ι → Sort ?u.185565
κ₂ : ι → Sort ?u.185570
κ' : ι' → Sort ?u.185575
S : Set (Set α)
f : α → β
⊢ f '' ⋂₀ S ⊆ ⋂ (s : Set α) (_ : s ∈ S), f '' s
rw [sInter_eq_biInter]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.185546
ι : Sort ?u.185549
ι' : Sort ?u.185552
ι₂ : Sort ?u.185555
κ : ι → Sort ?u.185560
κ₁ : ι → Sort ?u.185565
κ₂ : ι → Sort ?u.185570
κ' : ι' → Sort ?u.185575
S : Set (Set α)
f : α → β
⊢ (f '' ⋂ (i : Set α) (_ : i ∈ S), i) ⊆ ⋂ (s : Set α) (_ : s ∈ S), f '' s
apply image_iInter₂_subset