equiv

Mathlib.Control.Monad.Basic

URI: https://scilib.ai/kg/mathlib#StateT.equiv

Lean4

/-- reduce the equivalence between two state monads to the equivalence between
their respective function spaces -/
def equiv {σ₁ α₁ : Type u₀} {σ₂ α₂ : Type u₁} {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁}
    (F : (σ₁ → m₁ (α₁ × σ₁)) ≃ (σ₂ → m₂ (α₂ × σ₂))) : StateT σ₁ m₁ α₁ ≃ StateT σ₂ m₂ α₂ :=
  F

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

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

Разделы

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

Аффилиация

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