dist_mem_Icc_of_mem_tsupport_Ks

lemma dist_mem_Icc_of_mem_tsupport_Ks {s : ℤ} {x : X × X}    (h : x ∈ tsupport fun x ↦ (Ks s x.1 x.2)) :    dist x.1 x.2 ∈ Icc ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) := by  set C := support fun (x : X × X) ↦ Ks s x.1 x.2  have hcont : Continuous (fun (x : X × X) ↦ dist x.1 x.2) := by continuity  have hC : (fun (x : X × X) ↦ dist x.1 x.2) '' C ⊆ Icc ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) := by    intro r hr    simp only [mem_image, mem_support, C] at hr    obtain ⟨x, hx, rfl⟩ := hr    exact dist_mem_Icc_of_Ks_ne_zero hx  have hC' : (fun (x : X × X) ↦ dist x.1 x.2) '' (tsupport fun x ↦ Ks s x.1 x.2) ⊆      Icc ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) :=    subset_trans (image_closure_subset_closure_image hcont)      ((isClosed_Icc.closure_subset_iff).mpr hC)  exact hC' (mem_image_of_mem (fun x ↦ dist x.1 x.2) h)