limitRecOn_isMin — Mathlib

English

Simplified variant of succ limit recursion for not max with NoMaxOrder.

Русский

Упрощенное пределоведение для succ, если не максимум, при NoMaxOrder.

LaTeX

$$$\\mathrm{limitRecOn}(\\mathrm{Order.succ}(b)) = \\mathrm{succ}(b, \\neg IsMax(b)) (\\mathrm{limitRecOn}(b))$$$

Lean4

@[simp]
theorem limitRecOn_isMin (hb : IsMin b) : limitRecOn b isMin succ isSuccLimit = isMin b hb := by
  rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]

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