case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
a✝ : α
Hst✝ Hst : s ⊆ t
a : α
ha : a ∈ upperBounds s ∩ t
⊢ f a ∈ upperBounds (f '' s)
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
a : α
Hst✝ Hst : s ⊆ t
⊢ f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)
rintro _ ⟨a, ha, rfl⟩
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
a✝ : α
Hst✝ Hst : s ⊆ t
a : α
ha : a ∈ upperBounds s ∩ t
⊢ f a ∈ upperBounds (f '' s)
exact Hf.mem_upperBounds_image Hst ha.1 ha.2