src/HOL/Library/ContNotDenum.thy
changeset 59872 db4000b71fdb
parent 59720 f893472fff31
child 60308 f7e406aba90d
equal deleted inserted replaced
59871:e1a49ac9c537 59872:db4000b71fdb
   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 -