sigmaAll_apply — Mathlib

English

If φ is a bounded formula on n+1 variables, applying sigmaAll to ⟨n+1, φ⟩ yields ⟨n, φ.all⟩.

Русский

Применение sigmaAll к ⟨n+1, φ⟩ даёт ⟨n, φ.all⟩ для ограниченной формулы φ на n+1 переменных.

LaTeX

$$$\\sigmaAll(\\langle n+1, \\varphi \\rangle) = \\langle n, \\varphi_{all} \\rangle$$$

Lean4

@[simp]
theorem sigmaAll_apply {n} {φ : L.BoundedFormula α (n + 1)} : sigmaAll ⟨n + 1, φ⟩ = ⟨n, φ.all⟩ :=
  rfl

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