pred_findAtom — Mathlib

English

The predecessor of the atom findAtom r is the bottom element.

Русский

Предшественник атома findAtom r равен нулю.

LaTeX

$$Order.pred (findAtom r) = ⊥$$

Lean4

@[simp]
theorem pred_findAtom (r : α) : Order.pred (findAtom r) = ⊥ :=
  by
  unfold findAtom
  generalize h : Nat.find (bot_le (a := r)).exists_pred_iterate = n
  cases n
  · have : Order.pred^[0] r = ⊥ := by
      rw [← h]
      apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate
    simp only [Function.iterate_zero, id_eq] at this
    simp [this]
  · simp only [Nat.add_sub_cancel_right, ← Function.iterate_succ_apply', Nat.succ_eq_add_one]
    rw [← h]
    apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

Похожие утверждения