Standard Borel Structure on the Model Class #
This file shows that ModelsOf φ (the set of coded ℕ-models of an Lω₁ω sentence φ)
inherits StandardBorelSpace as a measurable subspace of the structure space.
Main Results #
modelsOf_isClopenable:ModelsOf φis clopenable (admits a finer Polish topology making it clopen).modelsOf_standardBorel: The subtype↥(ModelsOf φ)is standard Borel.
instance
FirstOrder.Language.modelsOf_standardBorel
{L : Language}
[L.IsRelational]
[Countable ((l : ℕ) × L.Relations l)]
(φ : L.Sentenceω)
:
The subtype of coded ℕ-models of φ is standard Borel: it inherits a standard Borel structure as a measurable subspace of the standard Borel structure space.