isSuccLimitRecOn_of_isSuccLimit — Mathlib

English

Dual statement to the SuccLimitRecOn_of_isSuccLimit, with pred and IsPredLimit.

Русский

Двойственное утверждение к SuccLimitRecOn_of_isSuccLimit.

LaTeX

$$$\\mathrm{isPredLimitRecOn}(b,\; isMax,\; pred,\; isPredLimit) = \\mathrm{isPredLimit}(b,hb)$ for $hb$ with IsPredLimit(b).$$

Lean4

@[simp]
theorem isSuccLimitRecOn_of_isSuccLimit (hb : IsSuccLimit b) :
    isSuccLimitRecOn b isMin succ isSuccLimit = isSuccLimit b hb := by
  rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_neg hb.not_isMin]

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