equal
deleted
inserted
replaced
1711 assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g" |
1711 assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g" |
1712 shows "quotient_map X X'' (g \<circ> f)" |
1712 shows "quotient_map X X'' (g \<circ> f)" |
1713 unfolding quotient_map_def |
1713 unfolding quotient_map_def |
1714 proof (intro conjI allI impI) |
1714 proof (intro conjI allI impI) |
1715 show "(g \<circ> f) ` topspace X = topspace X''" |
1715 show "(g \<circ> f) ` topspace X = topspace X''" |
1716 using assms image_comp unfolding quotient_map_def by force |
1716 using assms by (simp only: image_comp [symmetric]) (simp add: quotient_map_def) |
1717 next |
1717 next |
1718 fix U'' |
1718 fix U'' |
1719 assume "U'' \<subseteq> topspace X''" |
1719 assume "U'' \<subseteq> topspace X''" |
1720 define U' where "U' \<equiv> {y \<in> topspace X'. g y \<in> U''}" |
1720 define U' where "U' \<equiv> {y \<in> topspace X'. g y \<in> U''}" |
1721 have "U' \<subseteq> topspace X'" |
1721 have "U' \<subseteq> topspace X'" |