Topometric characterization of type spaces in continuous logic

James Hanson

def S : Type

Equations

• S = (↑(Set.Icc 0 1) × ℕ)

instance instTopologicalSpaceS : TopologicalSpace S

Equations

• instTopologicalSpaceS = instTopologicalSpaceProd

instance instMetricSpaceS : MetricSpace S

We prove that without the point at infinity, the metric in the proof of Example 1.2 really is a metric.

Equations

• instMetricSpaceS = MetricSpace.mk @instMetricSpaceS.proof_8