no goals
α : Type u_1
β : Type u_2
γ : Type ?u.38022
δ : Type ?u.38025
a b : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
x✝ : WithBot α
⊢ map f ⊥ ≤ map f x✝ ↔ ⊥ ≤ x✝
simp only [map_bot, bot_le]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.38022
δ : Type ?u.38025
a✝ b : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a : α
⊢ map f ↑a ≤ map f ⊥ ↔ ↑a ≤ ⊥
simp only [map_coe, map_bot, coe_ne_bot, not_coe_le_bot _]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.38022
δ : Type ?u.38025
a✝ b✝ : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a b : α
⊢ map f ↑a ≤ map f ↑b ↔ ↑a ≤ ↑b
simpa only [map_coe, coe_le_coe] using mono_iff