α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : ↑f ⊥ = ⊥
b : β
hb : ⊥ ⋖ ↑f b
⊢ ⊥ ⋖ b
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : ↑f ⊥ = ⊥
b : β
hb : IsAtom (↑f b)
⊢ IsAtom b
simp only [← bot_covby_iff] at hb ⊢
no goals
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : ↑f ⊥ = ⊥
b : β
hb : ⊥ ⋖ ↑f b
⊢ ⊥ ⋖ b
exact Covby.of_image f (hbot.symm ▸ hb)