realize_boundedFormula_top — Mathlib

English

Realizing a bounded formula at the top lattice is equivalent to realizing it after transporting to M via the top equivalence.

Русский

realizations ограниченной формулы на верхнем элементе эквивалентны реализациям после переноса в M через верхнее эквивалентное отображение.

LaTeX

$$$\forall α,n,φ, v, xs, φ.Realize v xs \leftrightarrow φ.Realize (⋯)$$$

Lean4

@[simp]
theorem realize_boundedFormula_top {α : Type*} {n : ℕ} {φ : L.BoundedFormula α n} {v : α → (⊤ : L.Substructure M)}
    {xs : Fin n → (⊤ : L.Substructure M)} : φ.Realize v xs ↔ φ.Realize (((↑) : _ → M) ∘ v) ((↑) ∘ xs) :=
  by
  rw [← StrongHomClass.realize_boundedFormula Substructure.topEquiv φ]
  simp

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