E : ℕ → Type ?u.303411
ι : Type u_1
inst✝¹ : Encodable ι
F : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ min ((1 / 2) ^ encode i) (dist (x i) (y i))
E : ℕ → Type ?u.303411
ι : Type u_1
inst✝¹ : Encodable ι
F : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
⊢ Summable fun i => min ((1 / 2) ^ encode i) (dist (x i) (y i))
refine summable_of_nonneg_of_le (fun i => ?_) (fun i => min_le_left _ _)
  summable_geometric_two_encode
no goals
E : ℕ → Type ?u.303411
ι : Type u_1
inst✝¹ : Encodable ι
F : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ min ((1 / 2) ^ encode i) (dist (x i) (y i))
exact le_min (pow_nonneg (by norm_num) _) dist_nonneg
no goals
E : ℕ → Type ?u.303411
ι : Type u_1
inst✝¹ : Encodable ι
F : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ 1 / 2
norm_num