no goals
α : Type u_1
β : Type u_2
γ : Type ?u.94162
δ : Type ?u.94165
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((Monotone fun a => map f ↑a) ∧ ∀ (x : α), map f ↑x ≤ map f ⊤) ↔ Monotone f
simp [Monotone]