src/HOL/Finite_Set.thy
changeset 41988 c2583bbb92f5
parent 41987 4ad8f1dc2e0b
child 42206 0920f709610f
equal deleted inserted replaced
41987:4ad8f1dc2e0b 41988:c2583bbb92f5
  1930 by (simp add: card_insert_if)
  1930 by (simp add: card_insert_if)
  1931 
  1931 
  1932 lemma card_Collect_less_nat[simp]: "card{i::nat. i < n} = n"
  1932 lemma card_Collect_less_nat[simp]: "card{i::nat. i < n} = n"
  1933 by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)
  1933 by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)
  1934 
  1934 
  1935 lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = n+1"
  1935 lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = Suc n"
  1936 using card_Collect_less_nat[of "Suc n"] by(simp add: less_Suc_eq_le)
  1936 using card_Collect_less_nat[of "Suc n"] by(simp add: less_Suc_eq_le)
  1937 
  1937 
  1938 lemma card_mono:
  1938 lemma card_mono:
  1939   assumes "finite B" and "A \<subseteq> B"
  1939   assumes "finite B" and "A \<subseteq> B"
  1940   shows "card A \<le> card B"
  1940   shows "card A \<le> card B"