realize_comp — Mathlib

English

If φ is atomic, then φ.Realize is preserved under composition with an embedding-like structure; that is, Realize is compatible with composition with coefficients of morphisms.

Русский

Если φ атомарна, то реализация сохраняется под композициями с морфизмами; реализация совместима с композициями коэффициентов морфизмов.

LaTeX

$$$\varphi.IsAtomic \to (\text{EmbeddingLike } F M N \to (\forall f, \varphi.Realize v xs \Rightarrow \varphi.Realize (f\circ v) (f\circ xs)))$$$

Lean4

theorem realize_comp {φ : L.BoundedFormula α n} (hA : φ.IsAtomic) [EmbeddingLike F M N] [L.HomClass F M N] (f : F)
    {v : α → M} {xs : Fin n → M} : φ.Realize v xs → φ.Realize (f ∘ v) (f ∘ xs) :=
  hA.realize_comp_of_injective (EmbeddingLike.injective f)

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