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