comp

Mathlib.ModelTheory.ElementaryMaps

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.ElementaryEmbedding.comp

Lean4

/-- Composition of elementary embeddings -/
@[trans]
def comp (hnp : N ↪ₑ[L] P) (hmn : M ↪ₑ[L] N) : M ↪ₑ[L] P
    where
  toFun := hnp ∘ hmn
  map_formula' n φ
    x := by
    obtain ⟨_, hhnp⟩ := hnp
    obtain ⟨_, hhmn⟩ := hmn
    erw [hhnp, hhmn]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru