isPredLimitRecOn_of_isMax — Mathlib

English

Recursion on pred given that b is a pred-limit equals the IsPredLimit data.

Русский

Рекурсия по pred при предельном состоянии b совпадает с данными IsPredLimit.

LaTeX

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

Lean4

theorem isPredLimitRecOn_of_isMax (hb : IsMax b) : isPredLimitRecOn b isMax pred isPredLimit = isMax b hb :=
  isSuccLimitRecOn_of_isMin (α := αᵒᵈ) isMax pred _ hb

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