English
Take the disjunction over a finite index set: iSup f is the finite join of the formulas f(b) over b in the universe of a finite type β.
Русский
Свернуть дизъюнктивность по сконченному индексу: iSup f — конечное объединение формул f(b) по всем b в универсе β.
LaTeX
$$$\\mathrm{iSup}\\; f = \\bigvee_{b \\in \\mathrm{univ}} f(b)$, когда β |Finite|.$$
Lean4
/-- Take the disjunction of a finite set of 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.BoundedFormula α n) : L.BoundedFormula α n :=
let _ := Fintype.ofFinite β
((Finset.univ : Finset β).toList.map f).foldr (· ⊔ ·) ⊥
