mem_age_of_equiv — Mathlib

English

If M is finitely generated and N ≃ N', then N' belongs to the age of M.

Русский

Если M конечносгенерирована и N ≃ N', то N' принадлежит возрасту M.

LaTeX

$${M,N : Bundled L.Structure} (h : FG L M) (MN : Nonempty (M ≃[L] N)) : N ∈ L.age M$$

Lean4

theorem mem_age_of_equiv {M N : Bundled L.Structure} (h : Structure.FG L M) (MN : Nonempty (M ≃[L] N)) : N ∈ L.age M :=
  ⟨MN.some.fg_iff.1 h, ⟨MN.some.symm.toEmbedding⟩⟩

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