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_reducible]

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