# HG changeset patch # User desharna # Date 1742815035 -3600 # Mon Mar 24 12:17:15 2025 +0100 # Node ID e2d7cf72c5523a594392177a218af17a9463b6dc # Parent fcd9b94def4d3c7c0d3c1dde56295c7d34974b17 fixed broken proof diff --git a/thys/Levy_Prokhorov_Metric/Prokhorov_Theorem.thy b/thys/Levy_Prokhorov_Metric/Prokhorov_Theorem.thy --- a/thys/Levy_Prokhorov_Metric/Prokhorov_Theorem.thy +++ b/thys/Levy_Prokhorov_Metric/Prokhorov_Theorem.thy @@ -245,7 +245,7 @@ have T_cont: "continuous_map (subtopology LPm.mtopology ?N) (subtopology Cb' B) T" unfolding continuous_map_in_subtopology proof - show "T ` topspace (subtopology LPm.mtopology ?N) \<subseteq> B" + show "T \<in> topspace (subtopology LPm.mtopology ?N) \<rightarrow> B" unfolding B_def Cb'_def proof safe fix N