equal
deleted
inserted
replaced
1704 lemma continuous_on_open_vimage: |
1704 lemma continuous_on_open_vimage: |
1705 "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> open (f -` B \<inter> s))" |
1705 "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> open (f -` B \<inter> s))" |
1706 unfolding continuous_on_open_invariant |
1706 unfolding continuous_on_open_invariant |
1707 by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s]) |
1707 by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s]) |
1708 |
1708 |
|
1709 corollary continuous_imp_open_vimage: |
|
1710 assumes "continuous_on s f" "open s" "open B" "f -` B \<subseteq> s" |
|
1711 shows "open (f -` B)" |
|
1712 by (metis assms continuous_on_open_vimage le_iff_inf) |
|
1713 |
1709 lemma continuous_on_closed_invariant: |
1714 lemma continuous_on_closed_invariant: |
1710 "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))" |
1715 "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))" |
1711 proof - |
1716 proof - |
1712 have *: "\<And>P Q::'b set\<Rightarrow>bool. (\<And>A. P A \<longleftrightarrow> Q (- A)) \<Longrightarrow> (\<forall>A. P A) \<longleftrightarrow> (\<forall>A. Q A)" |
1717 have *: "\<And>P Q::'b set\<Rightarrow>bool. (\<And>A. P A \<longleftrightarrow> Q (- A)) \<Longrightarrow> (\<forall>A. P A) \<longleftrightarrow> (\<forall>A. Q A)" |
1713 by (metis double_compl) |
1718 by (metis double_compl) |