Product Topology on the Structure Space

This file equips StructureSpace L with the product topology (from RelQuery L → Bool with Bool discrete) and proves that cylinder sets are clopen.

Main Results

• instTopologicalSpaceStructureSpace: Product topology on StructureSpace L.
• isClopen_relHolds: The set {c | c q = true} is clopen for each query q.
• isOpen_relHolds, isClosed_relHolds: Components of the clopen result.

instance FirstOrder.Language.instTopologicalSpaceStructureSpaceOn {L : Language} {α : Type u_1} : TopologicalSpace (L.StructureSpaceOn α)

Equations

• FirstOrder.Language.instTopologicalSpaceStructureSpaceOn = Pi.topologicalSpace

theorem FirstOrder.Language.isClopen_relHoldsOn {L : Language} {α : Type u_1} (q : L.RelQueryOn α) : IsClopen {c : L.StructureSpaceOn α | c q = true}

The set of codes where a given relation query returns true is clopen (generic).

instance FirstOrder.Language.instTopologicalSpaceStructureSpace {L : Language} : TopologicalSpace L.StructureSpace

StructureSpace L inherits the product topology from RelQuery L → Bool. Since Bool has the discrete topology, this is the product of discrete spaces.

Equations

• FirstOrder.Language.instTopologicalSpaceStructureSpace = Pi.topologicalSpace

theorem FirstOrder.Language.isClopen_relHolds {L : Language} (q : L.RelQuery) : IsClopen {c : L.StructureSpace | c q = true}

The set of codes where a given relation query returns true is clopen. This follows from the projection c ↦ c q being continuous and {true} being clopen in discrete Bool.

theorem FirstOrder.Language.isOpen_relHolds {L : Language} (q : L.RelQuery) : IsOpen {c : L.StructureSpace | c q = true}

The set of codes where a given relation query returns true is open.

theorem FirstOrder.Language.isClosed_relHolds {L : Language} (q : L.RelQuery) : IsClosed {c : L.StructureSpace | c q = true}

The set of codes where a given relation query returns true is closed.