(* Title: HOL/Cardinals/Fun_More.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
More on injections, bijections and inverses.
*)
section \<open>More on Injections, Bijections and Inverses\<close>
theory Fun_More
imports Main
begin
subsection \<open>Purely functional properties\<close>
(* unused *)
(*1*)lemma notIn_Un_bij_betw2:
assumes NIN: "b \ A" and NIN': "b' \ A'" and
BIJ: "bij_betw f A A'"
shows "bij_betw f (A \ {b}) (A' \ {b'}) = (f b = b')"
proof
assume "f b = b'"
thus "bij_betw f (A \ {b}) (A' \ {b'})"
using assms notIn_Un_bij_betw[of b A f A'] by auto
next
assume *: "bij_betw f (A \ {b}) (A' \ {b'})"
hence "f b \ A' \ {b'}"
unfolding bij_betw_def by auto
moreover
{assume "f b \ A'"
then obtain b1 where 1: "b1 \ A" and 2: "f b1 = f b" using BIJ
by (auto simp add: bij_betw_def)
hence "b = b1" using *
by (auto simp add: bij_betw_def inj_on_def)
with 1 NIN have False by auto
}
ultimately show "f b = b'" by blast
qed
(* unused *)
(*1*)lemma bij_betw_ball:
assumes BIJ: "bij_betw f A B"
shows "(\b \ B. phi b) = (\a \ A. phi(f a))"
using assms unfolding bij_betw_def inj_on_def by blast
(* unused *)
(*1*)lemma bij_betw_diff_singl:
assumes BIJ: "bij_betw f A A'" and IN: "a \ A"
shows "bij_betw f (A - {a}) (A' - {f a})"
proof-
let ?B = "A - {a}" let ?B' = "A' - {f a}"
have "f a \ A'" using IN BIJ unfolding bij_betw_def by blast
hence "a \ ?B \ f a \ ?B' \ A = ?B \ {a} \ A' = ?B' \ {f a}"
using IN by blast
thus ?thesis using notIn_Un_bij_betw3[of a ?B f ?B'] BIJ by simp
qed
subsection \<open>Properties involving finite and infinite sets\<close>
(* unused *)
(*1*)lemma bij_betw_inv_into_RIGHT:
assumes BIJ: "bij_betw f A A'" and SUB: "B' \ A'"
shows "f `((inv_into A f)`B') = B'"
using assms
proof(auto simp add: bij_betw_inv_into_right)
let ?f' = "(inv_into A f)"
fix a' assume *: "a' \<in> B'"
hence "a' \ A'" using SUB by auto
hence "a' = f (?f' a')"
using BIJ by (auto simp add: bij_betw_inv_into_right)
thus "a' \ f ` (?f' ` B')" using * by blast
qed
(* unused *)
(*1*)lemma bij_betw_inv_into_RIGHT_LEFT:
assumes BIJ: "bij_betw f A A'" and SUB: "B' \ A'" and
IM: "(inv_into A f) ` B' = B"
shows "f ` B = B'"
proof-
have "f`((inv_into A f)` B') = B'"
using assms bij_betw_inv_into_RIGHT[of f A A' B'] by auto
thus ?thesis using IM by auto
qed
(* unused *)
(*2*)lemma bij_betw_inv_into_twice:
assumes "bij_betw f A A'"
shows "\a \ A. inv_into A' (inv_into A f) a = f a"
proof
let ?f' = "inv_into A f" let ?f'' = "inv_into A' ?f'"
have 1: "bij_betw ?f' A' A" using assms
by (auto simp add: bij_betw_inv_into)
fix a assume *: "a \ A"
then obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
using 1 unfolding bij_betw_def by force
hence "?f'' a = a'"
using * 1 3 by (auto simp add: bij_betw_inv_into_left)
moreover have "f a = a'" using assms 2 3
by (auto simp add: bij_betw_inv_into_right)
ultimately show "?f'' a = f a" by simp
qed
subsection \<open>Properties involving Hilbert choice\<close>
(*1*)lemma bij_betw_inv_into_LEFT:
assumes BIJ: "bij_betw f A A'" and SUB: "B \ A"
shows "(inv_into A f)`(f ` B) = B"
using assms unfolding bij_betw_def using inv_into_image_cancel by force
(*1*)lemma bij_betw_inv_into_LEFT_RIGHT:
assumes BIJ: "bij_betw f A A'" and SUB: "B \ A" and
IM: "f ` B = B'"
shows "(inv_into A f) ` B' = B"
using assms bij_betw_inv_into_LEFT[of f A A' B] by fast
subsection \<open>Other facts\<close>
(*3*)lemma atLeastLessThan_injective:
assumes "{0 ..< m::nat} = {0 ..< n}"
shows "m = n"
proof-
{assume "m < n"
hence "m \ {0 ..< n}" by auto
hence "{0 ..< m} < {0 ..< n}" by auto
hence False using assms by blast
}
moreover
{assume "n < m"
hence "n \ {0 ..< m}" by auto
hence "{0 ..< n} < {0 ..< m}" by auto
hence False using assms by blast
}
ultimately show ?thesis by force
qed
(*2*)lemma atLeastLessThan_injective2:
"bij_betw f {0 ..< m::nat} {0 ..< n} \ m = n"
using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
card_atLeastLessThan[of m] card_atLeastLessThan[of n]
bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto
(*2*)lemma atLeastLessThan_less_eq:
"({0.. {0.. n)"
unfolding ivl_subset by arith
(*2*)lemma atLeastLessThan_less_eq2:
assumes "inj_on f {0..<(m::nat)} \ f ` {0.. {0..
shows "m \ n"
using assms
using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
card_atLeastLessThan[of m] card_atLeastLessThan[of n]
card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
(* unused *)
(*2*)lemma atLeastLessThan_less_eq3:
"(\f. inj_on f {0..<(m::nat)} \ f ` {0.. {0.. n)"
using atLeastLessThan_less_eq2
proof(auto)
assume "m \ n"
hence "inj_on id {0.. id ` {0.. {0..
thus "\f. inj_on f {0.. f ` {0.. {0..
qed
(* unused *)
(*3*)lemma atLeastLessThan_less:
"({0..
proof-
have "({0.. {0.. {0..
using subset_iff_psubset_eq by blast
also have "\ = (m \ n \ m ~= n)"
using atLeastLessThan_less_eq atLeastLessThan_injective by blast
also have "\ = (m < n)" by auto
finally show ?thesis .
qed
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
