sampleableExt

Mathlib.Testing.Plausible.Functions

URI: https://scilib.ai/kg/mathlib#Plausible.TotalFunction.DFinsupp.sampleableExt

Lean4

instance sampleableExt : SampleableExt (Π₀ _ : α, β)
    where
  proxy := TotalFunction α (SampleableExt.proxy β)
  interp := fun f => (f.comp SampleableExt.interp).applyFinsupp.toDFinsupp
  sample :=
    SampleableExt.sample (α := α → β)
      -- note: no way of shrinking the domain without an inverse to `interp`

  shrink :=
    {
      shrink :=
        letI : Shrinkable α := { };
        TotalFunction.shrink }

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

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

Разделы

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

Аффилиация

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