[STATEMENT]
lemma finer_than_iff_nhds:
  "T1 finer_than T2 \<longleftrightarrow> (\<forall>X. openin T2 X \<longrightarrow> openin T1 (X \<inter> topspace T1)) \<and> (topspace T1 \<subseteq> topspace T2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (T1 finer_than T2) = ((\<forall>X. openin T2 X \<longrightarrow> openin T1 (X \<inter> topspace T1)) \<and> topspace T1 \<subseteq> topspace T2)
[PROOF STEP]
by (auto simp: finer_than_def continuous_map_alt)