map_expansion — Mathlib

English

Relabeling of atomic bounded formulas remains atomic in the same general context.

Русский

Перепривязка атомарной ограниченной формулы сохраняет атомарность.

LaTeX

$$$\forall {L} {\alpha} {\beta} {m} (\varphi : L.BoundedFormula \alpha m), \varphi.IsAtomic \rightarrow \forall f : \alpha \to (\beta \oplus (\mathrm{Fin}~n)), (\varphi.relabel f).IsAtomic.$$$

Lean4

theorem map_expansion {L' : FirstOrder.Language} [L'.Structure M] (h : A.Definable L s) (φ : L →ᴸ L')
    [φ.IsExpansionOn M] : A.Definable L' s := by
  obtain ⟨ψ, rfl⟩ := h
  refine ⟨(φ.addConstants A).onFormula ψ, ?_⟩
  ext x
  simp only [mem_setOf_eq, LHom.realize_onFormula]

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