iSup

Mathlib.ModelTheory.Syntax

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Formula.iSup

Lean4

/-- Take the disjunction of finitely many formulas.

Note that this is an arbitrary formula defined using the axiom of choice. It is only well-defined up
to equivalence of formulas. -/
noncomputable def iSup [Finite α] (f : α → L.Formula β) : L.Formula β :=
  BoundedFormula.iSup f

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

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

Разделы

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

Аффилиация

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