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
ε : ℝ
p : Z
this : (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) = 0
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ 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
ε : ℝ
p : Z
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
have : (⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) = 0 := by
  have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ =>
    add_nonneg dist_nonneg dist_nonneg
  refine' le_antisymm _ (le_ciInf A)
  have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
  rw [this]
  exact ciInf_le ⟨0, forall_range_iff.2 A⟩ p
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
ε : ℝ
p : Z
this : (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) = 0
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
simp only [glueDist, this, zero_add]
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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) = 0
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
ε : ℝ
p : Z
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) = 0
have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ =>
  add_nonneg dist_nonneg dist_nonneg
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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) ≤ 0
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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) = 0
refine' le_antisymm _ (le_ciInf A)
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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) ≤ 0
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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) ≤ 0
have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) ≤ dist (Φ p) (Φ p) + dist (Ψ p) (Ψ 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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) ≤ 0
rw [this]
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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) ≤ dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
exact ciInf_le ⟨0, forall_range_iff.2 A⟩ p
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
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
simp