age_subset_age — Mathlib

English

If there is an L-embedding M ↪ N, then every finitely generated L-substructure of M also belongs to the age of N.

Русский

Если существует вложение M ↪ N, тогда каждая FG-подструктура M принадлежит возрасту N.

LaTeX

$$$\forall \ MN: M \hookrightarrow_L N,\ L.\mathrm{age}(M) \subseteq L.\mathrm{age}(N)$$$

Lean4

theorem age_subset_age (MN : M ↪[L] N) : L.age M ⊆ L.age N := fun _ => And.imp_right (Nonempty.map MN.comp)

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