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 : UniformSpace.toTopologicalSpace ≤ TopometricSpace.topology
• lowerSemiContinuous : ∀ (ε : ↑(Set.Ioi 0)), IsClosed {v : Fin 2 → X | dist (v 0) (v 1) ≤ ↑ε}

theorem TopometricSpace.refines {X : Type} [self : TopometricSpace X] : UniformSpace.toTopologicalSpace ≤ TopometricSpace.topology

theorem TopometricSpace.lowerSemiContinuous {X : Type} [self : TopometricSpace X] (ε : ↑(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 := UniformSpace.toTopologicalSpace, metric := m, refines := ⋯, lowerSemiContinuous := ⋯ }