cycle_eq

Mathlib.Data.Stream.Init

URI: https://scilib.ai/kg/mathlib#Stream'.cycle_eq

Lean4

theorem cycle_eq : ∀ (l : List α) (h : l ≠ []), cycle l h = l ++ₛ cycle l h
  | [], h => absurd rfl h
  | List.cons a l, _ =>
    have gen (l' a') :
      corec Stream'.cycleF Stream'.cycleG (a', l', a, l) =
        (a' :: l') ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l) :=
      by
      induction l' generalizing a' with
      | nil => rw [corec_eq]; rfl
      | cons a₁ l₁ ih => rw [corec_eq, Stream'.cycle_g_cons, ih a₁]; rfl
    gen l a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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