Topology on the space of complete types

This file defines a topological structure on the type CompleteType T α (note that these are types from model theory and not types from type theory). The topology is generated by sets of the form {p : CompleteType T α | ∃ φ, φ ∈ p}.

Note that the contents of this file are separate from Mathlib/ModelTheory/Types.lean to avoid importing files from the Topology folder there.

instance CompleteType.instTopologicalSpaceCompleteType {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} : TopologicalSpace (T.CompleteType α)

Equations

• CompleteType.instTopologicalSpaceCompleteType = TopologicalSpace.generateFrom (Set.range FirstOrder.Language.Theory.CompleteType.typesWith)

theorem CompleteType.isTopologicalBasis_range_typesWith {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} : TopologicalSpace.IsTopologicalBasis (Set.range FirstOrder.Language.Theory.CompleteType.typesWith)

theorem CompleteType.isOpen_typesWith {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} (φ : (L.withConstants α).Sentence) : IsOpen (FirstOrder.Language.Theory.CompleteType.typesWith φ)

theorem CompleteType.isClosed_typesWith {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} (φ : (L.withConstants α).Sentence) : IsClosed (FirstOrder.Language.Theory.CompleteType.typesWith φ)

theorem CompleteType.isClopen_typesWith {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} (φ : (L.withConstants α).Sentence) : IsClopen (FirstOrder.Language.Theory.CompleteType.typesWith φ)

instance CompleteType.instTotallySeparatedSpaceCompleteType {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} : TotallySeparatedSpace (T.CompleteType α)