iInf — Mathlib

English

Take the conjunction of a finite set of formulas: iInf f is the finite meet of f(b) over b in Finite β.

Русский

Свести конъюнкцию по конечному индексу: iInf f — конечное соединение формул f(b).

LaTeX

$$$\\mathrm{iInf}\\; f = \\bigwedge_{b \\in \\mathrm{univ}} f(b)$, когда β |Finite|.$$

Lean4

/-- Take the conjunction 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 iInf [Finite β] (f : β → L.BoundedFormula α n) : L.BoundedFormula α n :=
  let _ := Fintype.ofFinite β
  ((Finset.univ : Finset β).toList.map f).foldr (· ⊓ ·) ⊤

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