isMax_iterate_succ_of_eq_of_ne — Mathlib

English

Every element a is weakly covered by succ(a) in the same sense as before.

Русский

Каждый элемент a слабо покрывается succ(a) аналогично предыдущему случаю.

LaTeX

$$$\\forall a:\\alpha,\\ a \\mathrel{\\mathrm{WCovBy}} \\operatorname{succ}(a)$$$

Lean4

theorem isMax_iterate_succ_of_eq_of_ne {n m : ℕ} (h_eq : succ^[n] a = succ^[m] a) (h_ne : n ≠ m) : IsMax (succ^[n] a) :=
  by
  rcases le_total n m with h | h
  · exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)
  · rw [h_eq]
    exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

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