Theorems · Definition · general topology

Option.WeakEMetricSpace.OfIsOpenEmbedding

{α : Type u} →
  [t : TopologicalSpace α] →
    [inst : TopologicalSpace (Option α)] →
      [m : WeakEMetricSpace α] →
        [inst_1 : EDist (Option α)] →
          inst_1 = Option.toEDist → Topology.IsOpenEmbedding some → WeakEMetricSpace (Option α)

If some : α → Option α is an open embedding and α is has a weak pseudo extended metric structure, the structure extends naturally to Option α.

Defined in

Mathlib.Topology.EMetricSpace.Weak

Cited by

0 results in Mathlib

Foundations

Depth 147 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceWeakEMetricSpaceEDist