Some semilattices of definable sets in continuous logic

JAMES E. HANSON

Definition 1.1 defines a topometric space.

In the ordering of topologies, ⊥ is the discrete topology and τ₀ ≤ τ₁ means τ₀ refines τ₁, i.e., τ₀ ⊇ τ₁.

Note that neither the trivial ⊤ or discrete ⊥ topology can be paired with the usual metric on ℝ to form a topometric space; so the notion is subtle. We merely prove that if we use the same topology as that obtained from the metric then we always have a topometric space.

class TopometricSpace (X : Type) : Type

Topometric space structure on X.

• topology : TopologicalSpace X
• metric : MetricSpace X
• refines : PseudoMetricSpace.toUniformSpace.toTopologicalSpace ≤ topology
• lowerSemiContinuous (ε : ↑(Set.Ioi 0)) : IsClosed {v : Fin 2 → X | dist (v 0) (v 1) ≤ ↑ε}

def EasyTopometric (X : Type) [m : MetricSpace X] : TopometricSpace X

If we in particular let the topology be that obtained from the metric then we do have a topometric space.

Equations

• EasyTopometric X = { topology := PseudoMetricSpace.toUniformSpace.toTopologicalSpace, metric := m, refines := ⋯, lowerSemiContinuous := ⋯ }