isFraisse

Mathlib.ModelTheory.Fraisse

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

← MathLib Explorer

English

If a class has a Fraïssé limit, it is Fraisse.

Русский

Если класс имеет предел Фраиссe, он является Фраиссe.

LaTeX

$$[IsFraisseLimit] ⇒ IsFraisse$$

Lean4

/-- If a class has a Fraïssé limit, it must be Fraïssé. -/
theorem isFraisse [Countable (Σ l, L.Functions l)] [Countable M] (h : IsFraisseLimit K M) : IsFraisse K :=
  (congr rfl h.age).mp h.ultrahomogeneous.age_isFraisse

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

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

Разделы

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

Аффилиация

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