Definable₁

Mathlib.SetTheory.ZFC.Basic

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

Lean4

/-- An abbrev of `ZFSet.Definable` for unary functions. -/
abbrev Definable₁ (f : ZFSet.{u} → ZFSet.{u}) :=
  Definable 1 (fun s ↦ f (s 0))

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

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

Разделы

Аффилиация

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