boundedLimitRec_zero — Mathlib

English

Let l be a succ-limit ordinal. For any motive, the base value of boundedLimitRecOn at ⟨0, lLim.bot_lt⟩ is H1.

Русский

Пусть l — succ-предел ординала. Для любой мотивации базовое значение boundedLimitRecOn на ⟨0, lLim.bot_lt⟩ равно H1.

LaTeX

$$$$ \forall l\ (lLim : \mathrm{IsSuccLimit}\ l) \ {motive} \ (H_1\ H_2\ H_3):\; \mathrm{boundedLimitRecOn}(l, lLim, motive)\langle 0, lLim.bot\_lt \rangle H_1 H_2 H_3 = H_1 \,$$$

Lean4

@[simp]
theorem boundedLimitRec_zero {l} (lLim : IsSuccLimit l) {motive} (H₁ H₂ H₃) :
    @boundedLimitRecOn l lLim motive ⟨0, lLim.bot_lt⟩ H₁ H₂ H₃ = H₁ := by rw [boundedLimitRecOn, limitRecOn_zero]

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