realize_formula — Mathlib

English

If there is a strong homomorphism g, then realizability of a sentence φ is preserved: φ.Realize (g ∘ v) ↔ φ.Realize v.

Русский

Если существует сильный гомоморфизм g, то реализуемость предложения φ сохраняется: φ.Realize (g ∘ v) ↔ φ.Realize v.

LaTeX

$$$\varphi.Realize (g \circ v) \iff \varphi.Realize v$$$

Lean4

@[simp]
theorem realize_formula (φ : L.Formula α) {v : α → M} : φ.Realize (g ∘ v) ↔ φ.Realize v := by
  rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq, Unique.eq_default (g ∘ default)]

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