α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort ?u.16674
⊢ ¬IsSuccLimit (↑toDual a) ↔ ∃ b, ¬IsMin b ∧ pred b = a
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort ?u.16674
⊢ ¬IsPredLimit a ↔ ∃ b, ¬IsMin b ∧ pred b = a
rw [← isSuccLimit_toDual_iff]
no goals
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort ?u.16674
⊢ ¬IsSuccLimit (↑toDual a) ↔ ∃ b, ¬IsMin b ∧ pred b = a
exact not_isSuccLimit_iff