realize_all — Mathlib

English

Let θ be a bounded formula. The realization of all θ means θ holds for every element of the domain when the variable is extended by one step.

Русский

Пусть θ — ограниченная формула. Реализация all θ означает, что θ истинна для каждого элемента области при добавлении нового аргумента.

LaTeX

$$$ (\text{all } \theta)^{\mathcal{M}}(v, xs) \iff \forall a \in M, \theta^{\mathcal{M}}(v, \mathrm{Fin.snoc}(xs, a)) $$$

Lean4

@[simp]
theorem realize_all : (all θ).Realize v xs ↔ ∀ a : M, θ.Realize v (Fin.snoc xs a) :=
  Iff.rfl

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