α : Type u_1
β : Type ?u.6700
inst✝ : PartialOrder α
a b✝ : α
b : ↑(Ici a)
⊢ ⊥ ⋖ b ↔ a ⋖ ↑b
α : Type u_1
β : Type ?u.6700
inst✝ : PartialOrder α
a b✝ : α
b : ↑(Ici a)
⊢ IsAtom b ↔ a ⋖ ↑b
rw [← bot_covby_iff]
α : Type u_1
β : Type ?u.6700
inst✝ : PartialOrder α
a b✝ : α
b : ↑(Ici a)
⊢ OrdConnected (range ↑(OrderEmbedding.subtype fun c => a ≤ c))
α : Type u_1
β : Type ?u.6700
inst✝ : PartialOrder α
a b✝ : α
b : ↑(Ici a)
⊢ ⊥ ⋖ b ↔ a ⋖ ↑b
refine' (Set.OrdConnected.apply_covby_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) _).symm
no goals
α : Type u_1
β : Type ?u.6700
inst✝ : PartialOrder α
a b✝ : α
b : ↑(Ici a)
⊢ OrdConnected (range ↑(OrderEmbedding.subtype fun c => a ≤ c))
simpa only [OrderEmbedding.subtype_apply, Subtype.range_coe_subtype] using Set.ordConnected_Ici