instULiftable

Mathlib.Probability.ProbabilityMassFunction.Constructions

URI: https://scilib.ai/kg/mathlib#PMF.instULiftable

Lean4

/-- This instance allows `do` notation for `PMF` to be used across universes, for instance as
```lean4
example {R : Type u} [Ring R] (x : PMF ℕ) : PMF R := do
  let ⟨n⟩ ← ULiftable.up x
  pure n
```
where `x` is in universe `0`, but the return value is in universe `u`.
-/
instance : ULiftable PMF.{u} PMF.{v} where
  congr
    e :=
    { toFun := map e, invFun := map e.symm
      left_inv := fun a => by simp [map_comp, map_id]
      right_inv := fun a => by simp [map_comp, map_id] }

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

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

Разделы

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

Аффилиация

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