# HG changeset patch
# User nipkow
# Date 1516285266 -3600
# Node ID 867d7e91af653204fc5486cb4bdb8197d145635a
# Parent  afefc45ed4e957722355241e209c2e309f5e5b18
moved t3/t4 space from AFP/Gromov to here.

diff -r afefc45ed4e9 -r 867d7e91af65 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Jan 18 08:08:36 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Jan 18 15:21:06 2018 +0100
@@ -196,6 +196,27 @@
   using t0_space [of x y] by blast
 
 
+text \<open>A classical separation axiom for topological space, the T3 axiom -- also called regularity:
+if a point is not in a closed set, then there are open sets separating them.\<close>
+
+class t3_space = t2_space +
+  assumes t3_space: "closed S \<Longrightarrow> y \<notin> S \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}"
+
+text \<open>A classical separation axiom for topological space, the T4 axiom -- also called normality:
+if two closed sets are disjoint, then there are open sets separating them.\<close>
+
+class t4_space = t2_space +
+  assumes t4_space: "closed S \<Longrightarrow> closed T \<Longrightarrow> S \<inter> T = {} \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"
+
+text \<open>T4 is stronger than T3, and weaker than metric.\<close>
+
+instance t4_space \<subseteq> t3_space
+proof
+  fix S and y::'a assume "closed S" "y \<notin> S"
+  then show "\<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}"
+    using t4_space[of "{y}" S] by auto
+qed
+
 text \<open>A perfect space is a topological space with no isolated points.\<close>
 
 class perfect_space = topological_space +