get_of_bisim

Mathlib.Data.Stream.Init

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

Lean4

theorem get_of_bisim (bisim : IsBisimulation R) {s₁ s₂} :
    ∀ n, s₁ ~ s₂ → get s₁ n = get s₂ n ∧ drop (n + 1) s₁ ~ drop (n + 1) s₂
  | 0, h => bisim h
  | n + 1, h =>
    match bisim h with
    | ⟨_, trel⟩ => get_of_bisim bisim n trel

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

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

Разделы

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

Аффилиация

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