equal
deleted
inserted
replaced
108 by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def) |
108 by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def) |
109 thus ?thesis by auto |
109 thus ?thesis by auto |
110 qed |
110 qed |
111 |
111 |
112 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV" |
112 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV" |
113 using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan_tan) |
113 using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan) |
114 |
114 |
115 lemma uncountable_open_interval: |
115 lemma uncountable_open_interval: |
116 fixes a b :: real assumes ab: "a < b" |
116 fixes a b :: real assumes ab: "a < b" |
117 shows "uncountable {a<..<b}" |
117 shows "uncountable {a<..<b}" |
118 proof - |
118 proof - |