alls — Mathlib

English

The alls operation places universal quantifiers on all in-scope bound variables of a bounded formula, turning it into a plain first-order formula.

Русский

Операция alls добавляет универсальные кванторы над всеми соседними ограниченными переменными формулы.

LaTeX

$$$\text{alls}:\; \forall\{n\},\; L.BoundedFormula\alpha n \to L.Formula\alpha$ with the rule that 0-case is the identity and (n+1)-case prepends a universal quantifier to the inner formula.$$

Lean4

/-- Places universal quantifiers on all in-scope bound variables of a bounded formula. -/
def alls : ∀ {n}, L.BoundedFormula α n → L.Formula α
  | 0, φ => φ
  | _n + 1, φ => φ.all.alls

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