realize_onFormula — Mathlib

English

For any expansion φ from L to L' and any formula ψ in L, realization commutes with the onFormula construction.

Русский

Сведение к расширению наFormula сохраняется под реализацией равенства формул.

LaTeX

$$$ (\phi.onFormula \psi)^M(v) \iff \psi^M(v) $$$

Lean4

@[simp]
theorem realize_onFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α) {v : α → M} :
    (φ.onFormula ψ).Realize v ↔ ψ.Realize v :=
  φ.realize_onBoundedFormula ψ

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