convs'Aux_succ_none

Mathlib.Algebra.ContinuedFractions.Translations

URI: https://scilib.ai/kg/mathlib#GenContFract.convs'Aux_succ_none

English

If the head of s is none, then convs'Aux(s, n+1) = 0 for all n.

Русский

Если голова последовательности пуста, то convs'Aux(s, n+1) = 0 для всех n.

LaTeX

$$$ s.head = \\text{none} \\Rightarrow \\forall n,\\ convs'Aux\\, s\\ (n+1) = 0 $$$

Lean4

theorem convs'Aux_succ_none {s : Stream'.Seq (Pair K)} (h : s.head = none) (n : ℕ) : convs'Aux s (n + 1) = 0 := by
  simp [convs'Aux, h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru