terminatedAt_iff_s_terminatedAt

Mathlib.Algebra.ContinuedFractions.Translations

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

English

For any g and n, g.TerminatedAt n holds exactly when the underlying stream s satisfies g.s.TerminatedAt n.

Русский

Для любого g и n выполняется: g.TerminatedAt n тогда и только тогда, когда базовый поток s удовлетворяет g.s.TerminatedAt n.

LaTeX

$$$$ g.TerminatedAt n \iff g.s.TerminatedAt n. $$$$

Lean4

theorem terminatedAt_iff_s_terminatedAt : g.TerminatedAt n ↔ g.s.TerminatedAt n := by rfl

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

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

Разделы

Аффилиация

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