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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)
simp_rw [glueDist, add_add_add_comm _ ε, add_assoc]
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
refine le_ciInf_add fun p => ?_
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ (⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
rw [add_left_comm, add_assoc, ← two_mul]
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ (⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
refine le_ciInf_add fun q => ?_
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
rw [dist_comm z]
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
ε : ℝ
H : ∀ (p q : Z), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
linarith [dist_triangle4 x (Φ p) (Φ q) z, dist_triangle_left (Ψ p) (Ψ q) y, (abs_le.1 (H p q)).2]