Formal Textbook of Model Theory
1
Basic Definitions and Lemmas
▶
1.1
Vectors
1.2
Theories
2
Model Theory and The Rest of Mathlib
▶
2.1
Instances
2.2
Homomorphisms
3
Main Result
Dependency graph
3 Main Result
Theorem
3.0.1
✓
#
L∃∀N
Lean declarations
FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo
The theory of dense linear orders without endpoints is \(\aleph _0\)-categorical.
Proof
▶