IsExtensionPair

Mathlib.ModelTheory.PartialEquiv

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

Lean4

/-- Two structures `M` and `N` form an extension pair if the domain of any finitely-generated map
from `M` to `N` can be extended to include any element of `M`. -/
def IsExtensionPair : Prop :=
  ∀ (f : L.FGEquiv M N) (m : M), ∃ g, m ∈ g.1.dom ∧ f ≤ g

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

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

Разделы

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

Аффилиация

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