equal
deleted
inserted
replaced
118 lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)" |
118 lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)" |
119 by (rule compact_ssum, simp add: Rep_ssum_sinr) |
119 by (rule compact_ssum, simp add: Rep_ssum_sinr) |
120 |
120 |
121 lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x" |
121 lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x" |
122 unfolding compact_def |
122 unfolding compact_def |
123 by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinl]], simp) |
123 by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp) |
124 |
124 |
125 lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x" |
125 lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x" |
126 unfolding compact_def |
126 unfolding compact_def |
127 by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinr]], simp) |
127 by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp) |
128 |
128 |
129 lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x" |
129 lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x" |
130 by (safe elim!: compact_sinl compact_sinlD) |
130 by (safe elim!: compact_sinl compact_sinlD) |
131 |
131 |
132 lemma compact_sinr_iff [simp]: "compact (sinr\<cdot>x) = compact x" |
132 lemma compact_sinr_iff [simp]: "compact (sinr\<cdot>x) = compact x" |