α : Type u_1
β : Type ?u.7617
inst✝ : PartialOrder α
a✝ b : α
a : ↑(Iic b)
⊢ a ⋖ ⊤ ↔ ↑a ⋖ b
α : Type u_1
β : Type ?u.7617
inst✝ : PartialOrder α
a✝ b : α
a : ↑(Iic b)
⊢ IsCoatom a ↔ ↑a ⋖ b
rw [← covby_top_iff]
α : Type u_1
β : Type ?u.7617
inst✝ : PartialOrder α
a✝ b : α
a : ↑(Iic b)
⊢ OrdConnected (range ↑(OrderEmbedding.subtype fun c => c ≤ b))
α : Type u_1
β : Type ?u.7617
inst✝ : PartialOrder α
a✝ b : α
a : ↑(Iic b)
⊢ a ⋖ ⊤ ↔ ↑a ⋖ b
refine' (Set.OrdConnected.apply_covby_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) _).symm
no goals
α : Type u_1
β : Type ?u.7617
inst✝ : PartialOrder α
a✝ b : α
a : ↑(Iic b)
⊢ OrdConnected (range ↑(OrderEmbedding.subtype fun c => c ≤ b))
simpa only [OrderEmbedding.subtype_apply, Subtype.range_coe_subtype] using Set.ordConnected_Iic