isSatisfiable_directed_union_iff — Mathlib

English

A countably generated structure is ultrahomogeneous if and only if it has the universal extension property for triples (M ≤ N) and all finite partial isomorphisms extend.

Русский

Пусть структура счётно порождена: она ультрахомогенна тогда и только тогда, когда обладает свойством расширения для всех конечных частичных изоморфизмов.

LaTeX

$$$$ L.IsUltrahomogeneous M \\iff L.IsExtensionPair M M. $$$$

Lean4

theorem isSatisfiable_directed_union_iff {ι : Type*} [Nonempty ι] {T : ι → L.Theory} (h : Directed (· ⊆ ·) T) :
    Theory.IsSatisfiable (⋃ i, T i) ↔ ∀ i, (T i).IsSatisfiable :=
  by
  refine ⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => ?_⟩
  rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
  intro T0 hT0
  obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_biUnion hT0
  exact (h' i).mono hi

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