isSuccLimitRecOn_of_isMin — Mathlib

English

Dualized statement for pred with IsPredLimit.

Русский

Двойственное утверждение для pred с IsPredLimit.

LaTeX

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

Lean4

theorem isSuccLimitRecOn_of_isMin (hb : IsMin b) : isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb := by
  rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]

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