src/HOL/Library/Cardinality.thy
changeset 68011 fb6469cdf094
parent 67443 3abf6a722518
child 68028 1f9f973eed2a
     1.1 --- a/src/HOL/Library/Cardinality.thy	Fri Apr 20 07:36:58 2018 +0000
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Apr 20 07:36:59 2018 +0000
     1.3 @@ -27,9 +27,6 @@
     1.4  lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
     1.5    by (simp add: univ card_image inj_on_def Abs_inject)
     1.6  
     1.7 -lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)"
     1.8 -by(auto dest: finite_imageD intro: inj_Some)
     1.9 -
    1.10  lemma infinite_literal: "\<not> finite (UNIV :: String.literal set)"
    1.11  proof -
    1.12    have "inj STR" by(auto intro: injI)