English
For a Nontrivial linear order with a least element, the predicate P is forced by its truth on a single orbit generated by successors.
Русский
Для ненулевого линейного порядка с наименьшим элементом условие P распространяется по орбитам, порождаемым successor.
LaTeX
$$$ \forall P:\alpha \to \text{Prop},\ (\forall i, i \neq \bot \to P(i)) \iff (\forall i, P(\operatorname{succ} i)).$$$
Lean4
theorem forall_ne_bot_iff [Nontrivial α] [PartialOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α]
(P : α → Prop) : (∀ i, i ≠ ⊥ → P i) ↔ (∀ i, P (SuccOrder.succ i)) :=
by
refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩
obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose! hi; simp [hi]
rw [← Nat.succ_pred_eq_of_pos hj]
simp only [Function.iterate_succ', Function.comp_apply]
apply h
