realize_alls — Mathlib

English

For any bounded formula φ with n bound variables, φ.alls.Realize v is true exactly when φ.Realize v xs holds for every xs : Fin n → M.

Русский

Для любой ограниченной формулы φ с n ограничивающими переменными, φ.alls.Realize v истинно тогда и только тогда, когда для каждого xs : Fin n → M выполняется φ.Realize v xs.

LaTeX

$$$\forall {L} {M} {\varphi} (v)\, (\varphi.alls.Realize v) \iff \forall xs : \mathrm{Fin}~n \to M, \varphi.Realize v xs$$$

Lean4

@[simp]
theorem realize_alls {φ : L.BoundedFormula α n} {v : α → M} : φ.alls.Realize v ↔ ∀ xs : Fin n → M, φ.Realize v xs := by
  induction n with
  | zero => exact Unique.forall_iff.symm
  | succ n ih =>
    simp only [alls, ih, Realize]
    exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩

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