jointEmbedding — Mathlib

English

The age of M has joint embedding: any two members of L.age(M) can be jointly embedded into a larger structure in the age.

Русский

Возраст M обладает свойством совместной вложимости: любые две структуры из возраста могут быть встроены в общую структуру возраста.

LaTeX

$$JointEmbedding(L.age M)$$

Lean4

theorem jointEmbedding : JointEmbedding (L.age M) := fun _ hN _ hP =>
  ⟨Bundled.of (↥(hN.2.some.toHom.range ⊔ hP.2.some.toHom.range)),
    ⟨(fg_iff_structure_fg _).1 ((hN.1.range hN.2.some.toHom).sup (hP.1.range hP.2.some.toHom)),
      ⟨Substructure.subtype _⟩⟩,
    ⟨Embedding.comp (inclusion le_sup_left) hN.2.some.equivRange.toEmbedding⟩,
    ⟨Embedding.comp (inclusion le_sup_right) hP.2.some.equivRange.toEmbedding⟩⟩

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