terminatedAt_iff_partDen_none

Mathlib.Algebra.ContinuedFractions.Translations

URI: https://scilib.ai/kg/mathlib#GenContFract.terminatedAt_iff_partDen_none

English

For all n, g.TerminatedAt n iff g.partDens.get? n = none.

Русский

Для всех n: g.TerminatedAt n эквивално g.partDens.get? n = none.

LaTeX

$$$$ g.TerminatedAt n \iff g.partDens.get? n = none. $$$$

Lean4

theorem terminatedAt_iff_partDen_none : g.TerminatedAt n ↔ g.partDens.get? n = none := by
  rw [terminatedAt_iff_s_none, partDen_none_iff_s_none]

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

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

Разделы

Аффилиация

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