Theorems · Theorem · general topology

Metric.Sum.mem_uniformity_iff_glueDist

∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y}
  {ε : ℝ},
  0 < ε →
    ∀ (s : Set ((X ⊕ Y) × (X ⊕ Y))),
      s ∈ uniformity (X ⊕ Y) ↔ ∃ δ > 0, ∀ (a b : X ⊕ Y), Metric.glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

Defined in

Mathlib.Topology.MetricSpace.Gluing

Cited by

0 results in Mathlib

Foundations

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

Assumes

MetricSpaceMetricSpace