α : Type u_2
β : Type u_1
γ : Type ?u.48017
ι : Sort ?u.48020
π : α → Type ?u.48025
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ f '' s = t → SurjOn f s t ∧ MapsTo f s t
α : Type u_2
β : Type u_1
γ : Type ?u.48017
ι : Sort ?u.48020
π : α → Type ?u.48025
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t
refine' ⟨_, fun h => h.1.image_eq_of_mapsTo h.2⟩
α : Type u_2
β : Type u_1
γ : Type ?u.48017
ι : Sort ?u.48020
π : α → Type ?u.48025
s s₁ s₂ : Set α
t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)
α : Type u_2
β : Type u_1
γ : Type ?u.48017
ι : Sort ?u.48020
π : α → Type ?u.48025
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ f '' s = t → SurjOn f s t ∧ MapsTo f s t
rintro rfl
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.48017
ι : Sort ?u.48020
π : α → Type ?u.48025
s s₁ s₂ : Set α
t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)
exact ⟨s.surjOn_image f, s.mapsTo_image f⟩