lawfulFix'

Mathlib.Control.LawfulFix

URI: https://scilib.ai/kg/mathlib#Pi.lawfulFix'

Lean4

instance lawfulFix' [LawfulFix <| (x : Sigma β) → γ x.1 x.2] : LawfulFix ((x y : _) → γ x y) where
  fix_eq {_f}
    hc := by
    dsimp [fix]
    conv_lhs => erw [LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)]
    rfl

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

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

Разделы

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

Аффилиация

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