subtype

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primcodable.subtype

Lean4

/-- A subtype of a primitive recursive predicate is `Primcodable`. -/
def subtype {p : α → Prop} [DecidablePred p] (hp : PrimrecPred p) : Primcodable (Subtype p) :=
  ⟨have : Primrec fun n => (@decode α _ n).bind fun a => Option.guard p a :=
      option_bind .decode (option_guard (hp.comp snd).primrecRel snd)
    nat_iff.1 <|
      (encode_iff.2 this).of_eq fun n =>
        show _ = encode ((@decode α _ n).bind fun _ => _)
          by
          rcases @decode α _ n with - | a; · rfl
          dsimp [Option.guard]
          by_cases h : p a <;> simp [h]; rfl⟩

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

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

Разделы

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

Аффилиация

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