isSuccPrelimitRecOn_of_isSuccPrelimit

English

If b is a succPrelimit, then the recursive construction equals the given isSuccPrelimit value.

Русский

Если b является succPrelimit, то рекурсивное построение равно заданному значению isSuccPrelimit.

LaTeX

$$hb : IsSuccPrelimit b -> isSuccPrelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb$$

Lean4

theorem isSuccPrelimitRecOn_of_isSuccPrelimit (hb : IsSuccPrelimit b) :
    isSuccPrelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb :=
  dif_pos hb

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