out

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.Definable₂.out

Lean4

/-- Turns a binary definable function into a binary `PSet` function. -/
abbrev out (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f] : PSet.{u} → PSet.{u} → PSet.{u} := fun x y ↦
  Definable.out (fun s ↦ f (s 0) (s 1)) ![x, y]

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

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

Разделы

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

Аффилиация

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