English
The theory of dense linear orders is ω-complete (indeed ω-categorical).
Русский
Теория плотных линейных порядков является ω-дополненной (на самом деле ω-однозначной).
LaTeX
$$$ \text{DLO IsComplete} $$$
Lean4
theorem dlo_age [Language.order.Structure M] [Mdlo : M ⊨ Language.order.dlo] [Nonempty M] :
Language.order.age M =
{M : CategoryTheory.Bundled.{w'} Language.order.Structure | Finite M ∧ M ⊨ Language.order.linearOrderTheory} :=
by
classical
rw [age]
ext N
refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩, fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
letI := Language.order.linearOrderOfModels M
letI := Language.order.linearOrderOfModels N
exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩
