X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
let i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
let _ := i.toUniformSpace
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ (toGlueL hΦ hΨ ∘ Φ) x✝ = (toGlueR hΦ hΨ ∘ Ψ) x✝
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
funext
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ Quotient.mk'' (Sum.inl (Φ x✝)) = Quotient.mk'' (Sum.inr (Ψ x✝))
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ (toGlueL hΦ hΨ ∘ Φ) x✝ = (toGlueR hΦ hΨ ∘ Ψ) x✝
simp only [comp, toGlueL, toGlueR]
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ dist (Sum.inl (Φ x✝)) (Sum.inr (Ψ x✝)) = 0
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ Quotient.mk'' (Sum.inl (Φ x✝)) = Quotient.mk'' (Sum.inr (Ψ x✝))
refine' UniformSpace.SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 _)
no goals
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ dist (Sum.inl (Φ x✝)) (Sum.inr (Ψ x✝)) = 0
exact glueDist_glued_points Φ Ψ 0 _