Theorems · Definition · general topology

Metric.glueDist

{X : Type u} →
  {Y : Type v} → {Z : Type w} → [MetricSpace X] → [MetricSpace Y] → (Z → X) → (Z → Y) → ℝ → X ⊕ Y → X ⊕ Y → ℝ

Define a predistance on X ⊕ Y, for which Φ p and Ψ p are at distance ε

Defined in

Mathlib.Topology.MetricSpace.Gluing

Cited by

6 results in Mathlib

Foundations

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

Assumes

MetricSpaceMetricSpace