equal
deleted
inserted
replaced
648 qed |
648 qed |
649 then show ?thesis using B(1) by auto |
649 then show ?thesis using B(1) by auto |
650 qed |
650 qed |
651 |
651 |
652 |
652 |
653 subsection%important \<open>Polish spaces\<close> |
653 subsection \<open>Polish spaces\<close> |
654 |
654 |
655 text \<open>Textbooks define Polish spaces as completely metrizable. |
655 text \<open>Textbooks define Polish spaces as completely metrizable. |
656 We assume the topology to be complete for a given metric.\<close> |
656 We assume the topology to be complete for a given metric.\<close> |
657 |
657 |
658 class polish_space = complete_space + second_countable_topology |
658 class polish_space = complete_space + second_countable_topology |