limitRecOn_isMax — Mathlib

English

If b is maximal, the limit-recursion value equals the maximal-value function at b.

Русский

Если b является максимальным, то значение limitRecOn совпадает с функцией максимума на b.

LaTeX

$$$\\text{limitRecOn}(b, isMax, pred, isPredLimit) = \\text{isMax}(b)(\\mathrm{hb})$$$

Lean4

@[simp]
theorem limitRecOn_isMax (hb : IsMax b) : limitRecOn b isMax pred isPredLimit = isMax b hb :=
  SuccOrder.limitRecOn_isMin (α := αᵒᵈ) isMax pred _ hb

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