map_formula — Mathlib

English

If f is an elementary embedding of L-structures, then for any formula φ and map x, φ is realized the same after applying f to x: φ.Realize (f ∘ x) iff φ.Realize x.

Русский

Если f есть элементарное вложение структур L, то для любой формулы φ и отображения x: φ.Realize (f ∘ x) эквивалентно φ.Realize x.

LaTeX

$$$\\varphi.Realize (f \\circ x) \\iff \\varphi.Realize x$$$

Lean4

@[simp]
theorem map_formula (f : M ↪ₑ[L] N) {α : Type*} (φ : L.Formula α) (x : α → M) : φ.Realize (f ∘ x) ↔ φ.Realize x := by
  rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]

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