equiv

Mathlib.Control.Monad.Basic

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

Lean4

/-- reduce the equivalence between two reader 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₂ α₂)) : ReaderT ρ₁ m₁ α₁ ≃ ReaderT ρ₂ m₂ α₂ :=
  F

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

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

Разделы

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

Аффилиация

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