English
The age of a dense linear order is the set of all finite linear orders (finite models of linear order theory).
Русский
age плотного линейного порядка состоит из всех конечных линейных порядков (конечных моделей теории порядка).
LaTeX
$$$ \operatorname{age}(M) = \{ M' : \text{Finite } M' \wedge M' \models \text{linearOrderTheory} \}$$$
Lean4
theorem dlo_isExtensionPair (M : Type w) [Language.order.Structure M] [M ⊨ Language.order.linearOrderTheory]
(N : Type w') [Language.order.Structure N] [N ⊨ Language.order.dlo] [Nonempty N] :
Language.order.IsExtensionPair M N := by
classical
rw [isExtensionPair_iff_exists_embedding_closure_singleton_sup]
intro S S_fg f m
letI := Language.order.linearOrderOfModels M
letI := Language.order.linearOrderOfModels N
have := Language.order.denselyOrdered_of_dlo N
have := Language.order.noBotOrder_of_dlo N
have := Language.order.noTopOrder_of_dlo N
have := NoBotOrder.to_noMinOrder N
have := NoTopOrder.to_noMaxOrder N
have hS : Set.Finite (S : Set M) := (S.fg_iff_structure_fg.1 S_fg).finite
obtain ⟨g, hg⟩ :=
Order.exists_orderEmbedding_insert hS.toFinset
((OrderIso.setCongr hS.toFinset (S : Set M) hS.coe_toFinset).toOrderEmbedding.trans
(OrderEmbedding.ofStrictMono f (HomClass.strictMono f)))
m
let g' : ((Substructure.closure Language.order).toFun { m } ⊔ S : Language.order.Substructure M) ↪o N :=
((OrderIso.setCongr _ _
(by
convert
LowerAdjoint.closure_eq_self_of_mem_closed _
(Substructure.mem_closed_of_isRelational Language.order ((insert m hS.toFinset : Finset M) : Set M))
simp only [Finset.coe_insert, Set.Finite.coe_toFinset, Substructure.closure_insert,
Substructure.closure_eq])).toOrderEmbedding.trans
g)
use StrongHomClass.toEmbedding g'
ext ⟨x, xS⟩
refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩
simp only [Set.Finite.mem_toFinset, SetLike.mem_coe, xS]
