no goals
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x y : X
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inl y) = 0
⊢ Sum.inl x = Sum.inl y
rw [eq_of_dist_eq_zero h]
case h
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ False
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ Sum.inl x = Sum.inr y
exfalso
no goals
case h
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ False
linarith [le_glueDist_inl_inr Φ Ψ ε x y]
case h
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ False
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ Sum.inr x = Sum.inl y
exfalso
no goals
case h
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ False
linarith [le_glueDist_inr_inl Φ Ψ ε x y]
no goals
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x y : Y
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inr y) = 0
⊢ Sum.inr x = Sum.inr y
rw [eq_of_dist_eq_zero h]