|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Selection.thy
Sprache: Isabelle
|
|
(* Title: HOL/BNF_Cardinal_Order_Relation.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
Cardinal-order relations as needed by bounded natural functors.
*)
section \<open>Cardinal-Order Relations as Needed by Bounded Natural Functors\<close>
theory BNF_Cardinal_Order_Relation
imports Zorn BNF_Wellorder_Constructions
begin
text\<open>In this section, we define cardinal-order relations to be minim well-orders
on their field. Then we define the cardinal of a set to be {\em some} cardinal-order
relation on that set, which will be unique up to order isomorphism. Then we study
the connection between cardinals and:
\begin{itemize}
\item standard set-theoretic constructions: products,
sums, unions, lists, powersets, set-of finite sets operator;
\item finiteness and infiniteness (in particular, with the numeric cardinal operator
for finite sets, \<open>card\<close>, from the theory \<open>Finite_Sets.thy\<close>).
\end{itemize}
%
On the way, we define the canonical $\omega$ cardinal and finite cardinals. We also
define (again, up to order isomorphism) the successor of a cardinal, and show that
any cardinal admits a successor.
Main results of this section are the existence of cardinal relations and the
facts that, in the presence of infiniteness,
most of the standard set-theoretic constructions (except for the powerset)
{\em do not increase cardinality}. In particular, e.g., the set of words/lists over
any infinite set has the same cardinality (hence, is in bijection) with that set.
\<close>
subsection \<open>Cardinal orders\<close>
text\<open>A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
order-embedding relation, \<open>\<le>o\<close> (which is the same as being {\em minimal} w.r.t. the
strict order-embedding relation, \<open><o\<close>), among all the well-orders on its field.\<close>
definition card_order_on :: "'a set \ 'a rel \ bool"
where
"card_order_on A r \ well_order_on A r \ (\r'. well_order_on A r' \ r \o r')"
abbreviation "Card_order r \ card_order_on (Field r) r"
abbreviation "card_order r \ card_order_on UNIV r"
lemma card_order_on_well_order_on:
assumes "card_order_on A r"
shows "well_order_on A r"
using assms unfolding card_order_on_def by simp
lemma card_order_on_Card_order:
"card_order_on A r \ A = Field r \ Card_order r"
unfolding card_order_on_def using well_order_on_Field by blast
text\<open>The existence of a cardinal relation on any given set (which will mean
that any set has a cardinal) follows from two facts:
\begin{itemize}
\item Zermelo's theorem (proved in \<open>Zorn.thy\<close> as theorem \<open>well_order_on\<close>),
which states that on any given set there exists a well-order;
\item The well-founded-ness of \<open><o\<close>, ensuring that then there exists a minimal
such well-order, i.e., a cardinal order.
\end{itemize}
\<close>
theorem card_order_on: "\r. card_order_on A r"
proof-
obtain R where R_def: "R = {r. well_order_on A r}" by blast
have 1: "R \ {} \ (\r \ R. Well_order r)"
using well_order_on[of A] R_def well_order_on_Well_order by blast
hence "\r \ R. \r' \ R. r \o r'"
using exists_minim_Well_order[of R] by auto
thus ?thesis using R_def unfolding card_order_on_def by auto
qed
lemma card_order_on_ordIso:
assumes CO: "card_order_on A r" and CO': "card_order_on A r'"
shows "r =o r'"
using assms unfolding card_order_on_def
using ordIso_iff_ordLeq by blast
lemma Card_order_ordIso:
assumes CO: "Card_order r" and ISO: "r' =o r"
shows "Card_order r'"
using ISO unfolding ordIso_def
proof(unfold card_order_on_def, auto)
fix p' assume "well_order_on (Field r') p'"
hence 0: "Well_order p' \ Field p' = Field r'"
using well_order_on_Well_order by blast
obtain f where 1: "iso r' r f" and 2: "Well_order r \ Well_order r'"
using ISO unfolding ordIso_def by auto
hence 3: "inj_on f (Field r') \ f ` (Field r') = Field r"
by (auto simp add: iso_iff embed_inj_on)
let ?p = "dir_image p' f"
have 4: "p' =o ?p \ Well_order ?p"
using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
moreover have "Field ?p = Field r"
using 0 3 by (auto simp add: dir_image_Field)
ultimately have "well_order_on (Field r) ?p" by auto
hence "r \o ?p" using CO unfolding card_order_on_def by auto
thus "r' \o p'"
using ISO 4 ordLeq_ordIso_trans ordIso_ordLeq_trans ordIso_symmetric by blast
qed
lemma Card_order_ordIso2:
assumes CO: "Card_order r" and ISO: "r =o r'"
shows "Card_order r'"
using assms Card_order_ordIso ordIso_symmetric by blast
subsection \<open>Cardinal of a set\<close>
text\<open>We define the cardinal of set to be {\em some} cardinal order on that set.
We shall prove that this notion is unique up to order isomorphism, meaning
that order isomorphism shall be the true identity of cardinals.\<close>
definition card_of :: "'a set \ 'a rel" ("|_|" )
where "card_of A = (SOME r. card_order_on A r)"
lemma card_of_card_order_on: "card_order_on A |A|"
unfolding card_of_def by (auto simp add: card_order_on someI_ex)
lemma card_of_well_order_on: "well_order_on A |A|"
using card_of_card_order_on card_order_on_def by blast
lemma Field_card_of: "Field |A| = A"
using card_of_card_order_on[of A] unfolding card_order_on_def
using well_order_on_Field by blast
lemma card_of_Card_order: "Card_order |A|"
by (simp only: card_of_card_order_on Field_card_of)
corollary ordIso_card_of_imp_Card_order:
"r =o |A| \ Card_order r"
using card_of_Card_order Card_order_ordIso by blast
lemma card_of_Well_order: "Well_order |A|"
using card_of_Card_order unfolding card_order_on_def by auto
lemma card_of_refl: "|A| =o |A|"
using card_of_Well_order ordIso_reflexive by blast
lemma card_of_least: "well_order_on A r \ |A| \o r"
using card_of_card_order_on unfolding card_order_on_def by blast
lemma card_of_ordIso:
"(\f. bij_betw f A B) = ( |A| =o |B| )"
proof(auto)
fix f assume *: "bij_betw f A B"
then obtain r where "well_order_on B r \ |A| =o r"
using Well_order_iso_copy card_of_well_order_on by blast
hence "|B| \o |A|" using card_of_least
ordLeq_ordIso_trans ordIso_symmetric by blast
moreover
{let ?g = "inv_into A f"
have "bij_betw ?g B A" using * bij_betw_inv_into by blast
then obtain r where "well_order_on A r \ |B| =o r"
using Well_order_iso_copy card_of_well_order_on by blast
hence "|A| \o |B|" using card_of_least
ordLeq_ordIso_trans ordIso_symmetric by blast
}
ultimately show "|A| =o |B|" using ordIso_iff_ordLeq by blast
next
assume "|A| =o |B|"
then obtain f where "iso ( |A| ) ( |B| ) f"
unfolding ordIso_def by auto
hence "bij_betw f A B" unfolding iso_def Field_card_of by simp
thus "\f. bij_betw f A B" by auto
qed
lemma card_of_ordLeq:
"(\f. inj_on f A \ f ` A \ B) = ( |A| \o |B| )"
proof(auto)
fix f assume *: "inj_on f A" and **: "f ` A \ B"
{assume "|B|
hence "|B| \o |A|" using ordLeq_iff_ordLess_or_ordIso by blast
then obtain g where "embed ( |B| ) ( |A| ) g"
unfolding ordLeq_def by auto
hence 1: "inj_on g B \ g ` B \ A" using embed_inj_on[of "|B|" "|A|" "g"]
card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"]
embed_Field[of "|B|" "|A|" g] by auto
obtain h where "bij_betw h A B"
using * ** 1 Schroeder_Bernstein[of f] by fastforce
hence "|A| =o |B|" using card_of_ordIso by blast
hence "|A| \o |B|" using ordIso_iff_ordLeq by auto
}
thus "|A| \o |B|" using ordLess_or_ordLeq[of "|B|" "|A|"]
by (auto simp: card_of_Well_order)
next
assume *: "|A| \o |B|"
obtain f where "embed ( |A| ) ( |B| ) f"
using * unfolding ordLeq_def by auto
hence "inj_on f A \ f ` A \ B" using embed_inj_on[of "|A|" "|B|" f]
card_of_Well_order[of "A"] Field_card_of[of "A"] Field_card_of[of "B"]
embed_Field[of "|A|" "|B|" f] by auto
thus "\f. inj_on f A \ f ` A \ B" by auto
qed
lemma card_of_ordLeq2:
"A \ {} \ (\g. g ` B = A) = ( |A| \o |B| )"
using card_of_ordLeq[of A B] inj_on_iff_surj[of A B] by auto
lemma card_of_ordLess:
"(\(\f. inj_on f A \ f ` A \ B)) = ( |B|
proof-
have "(\(\f. inj_on f A \ f ` A \ B)) = (\ |A| \o |B| )"
using card_of_ordLeq by blast
also have "\ = ( |B|
using card_of_Well_order[of A] card_of_Well_order[of B]
not_ordLeq_iff_ordLess by blast
finally show ?thesis .
qed
lemma card_of_ordLess2:
"B \ {} \ (\(\f. f ` A = B)) = ( |A|
using card_of_ordLess[of B A] inj_on_iff_surj[of B A] by auto
lemma card_of_ordIsoI:
assumes "bij_betw f A B"
shows "|A| =o |B|"
using assms unfolding card_of_ordIso[symmetric] by auto
lemma card_of_ordLeqI:
assumes "inj_on f A" and "\ a. a \ A \ f a \ B"
shows "|A| \o |B|"
using assms unfolding card_of_ordLeq[symmetric] by auto
lemma card_of_unique:
"card_order_on A r \ r =o |A|"
by (simp only: card_order_on_ordIso card_of_card_order_on)
lemma card_of_mono1:
"A \ B \ |A| \o |B|"
using inj_on_id[of A] card_of_ordLeq[of A B] by fastforce
lemma card_of_mono2:
assumes "r \o r'"
shows "|Field r| \o |Field r'|"
proof-
obtain f where
1: "well_order_on (Field r) r \ well_order_on (Field r) r \ embed r r' f"
using assms unfolding ordLeq_def
by (auto simp add: well_order_on_Well_order)
hence "inj_on f (Field r) \ f ` (Field r) \ Field r'"
by (auto simp add: embed_inj_on embed_Field)
thus "|Field r| \o |Field r'|" using card_of_ordLeq by blast
qed
lemma card_of_cong: "r =o r' \ |Field r| =o |Field r'|"
by (simp add: ordIso_iff_ordLeq card_of_mono2)
lemma card_of_Field_ordLess: "Well_order r \ |Field r| \o r"
using card_of_least card_of_well_order_on well_order_on_Well_order by blast
lemma card_of_Field_ordIso:
assumes "Card_order r"
shows "|Field r| =o r"
proof-
have "card_order_on (Field r) r"
using assms card_order_on_Card_order by blast
moreover have "card_order_on (Field r) |Field r|"
using card_of_card_order_on by blast
ultimately show ?thesis using card_order_on_ordIso by blast
qed
lemma Card_order_iff_ordIso_card_of:
"Card_order r = (r =o |Field r| )"
using ordIso_card_of_imp_Card_order card_of_Field_ordIso ordIso_symmetric by blast
lemma Card_order_iff_ordLeq_card_of:
"Card_order r = (r \o |Field r| )"
proof-
have "Card_order r = (r =o |Field r| )"
unfolding Card_order_iff_ordIso_card_of by simp
also have "... = (r \o |Field r| \ |Field r| \o r)"
unfolding ordIso_iff_ordLeq by simp
also have "... = (r \o |Field r| )"
using card_of_Field_ordLess
by (auto simp: card_of_Field_ordLess ordLeq_Well_order_simp)
finally show ?thesis .
qed
lemma Card_order_iff_Restr_underS:
assumes "Well_order r"
shows "Card_order r = (\a \ Field r. Restr r (underS r a)
using assms unfolding Card_order_iff_ordLeq_card_of
using ordLeq_iff_ordLess_Restr card_of_Well_order by blast
lemma card_of_underS:
assumes r: "Card_order r" and a: "a \ Field r"
shows "|underS r a|
proof-
let ?A = "underS r a" let ?r' = "Restr r ?A"
have 1: "Well_order r"
using r unfolding card_order_on_def by simp
have "Well_order ?r'" using 1 Well_order_Restr by auto
moreover have "card_order_on (Field ?r') |Field ?r'|"
using card_of_card_order_on .
ultimately have "|Field ?r'| \o ?r'"
unfolding card_order_on_def by simp
moreover have "Field ?r' = ?A"
using 1 wo_rel.underS_ofilter Field_Restr_ofilter
unfolding wo_rel_def by fastforce
ultimately have "|?A| \o ?r'" by simp
also have "?r'
using 1 a r Card_order_iff_Restr_underS by blast
also have "|Field r| =o r"
using r ordIso_symmetric unfolding Card_order_iff_ordIso_card_of by auto
finally show ?thesis .
qed
lemma ordLess_Field:
assumes "r
shows "|Field r|
proof-
have "well_order_on (Field r) r" using assms unfolding ordLess_def
by (auto simp add: well_order_on_Well_order)
hence "|Field r| \o r" using card_of_least by blast
thus ?thesis using assms ordLeq_ordLess_trans by blast
qed
lemma internalize_card_of_ordLeq:
"( |A| \o r) = (\B \ Field r. |A| =o |B| \ |B| \o r)"
proof
assume "|A| \o r"
then obtain p where 1: "Field p \ Field r \ |A| =o p \ p \o r"
using internalize_ordLeq[of "|A|" r] by blast
hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
hence "|Field p| =o p" using card_of_Field_ordIso by blast
hence "|A| =o |Field p| \ |Field p| \o r"
using 1 ordIso_equivalence ordIso_ordLeq_trans by blast
thus "\B \ Field r. |A| =o |B| \ |B| \o r" using 1 by blast
next
assume "\B \ Field r. |A| =o |B| \ |B| \o r"
thus "|A| \o r" using ordIso_ordLeq_trans by blast
qed
lemma internalize_card_of_ordLeq2:
"( |A| \o |C| ) = (\B \ C. |A| =o |B| \ |B| \o |C| )"
using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto
subsection \<open>Cardinals versus set operations on arbitrary sets\<close>
text\<open>Here we embark in a long journey of simple results showing
that the standard set-theoretic operations are well-behaved w.r.t. the notion of
cardinal -- essentially, this means that they preserve the ``cardinal identity"
\<open>=o\<close> and are monotonic w.r.t. \<open>\<le>o\<close>.
\<close>
lemma card_of_empty: "|{}| \o |A|"
using card_of_ordLeq inj_on_id by blast
lemma card_of_empty1:
assumes "Well_order r \ Card_order r"
shows "|{}| \o r"
proof-
have "Well_order r" using assms unfolding card_order_on_def by auto
hence "|Field r| <=o r"
using assms card_of_Field_ordLess by blast
moreover have "|{}| \o |Field r|" by (simp add: card_of_empty)
ultimately show ?thesis using ordLeq_transitive by blast
qed
corollary Card_order_empty:
"Card_order r \ |{}| \o r" by (simp add: card_of_empty1)
lemma card_of_empty2:
assumes LEQ: "|A| =o |{}|"
shows "A = {}"
using assms card_of_ordIso[of A] bij_betw_empty2 by blast
lemma card_of_empty3:
assumes LEQ: "|A| \o |{}|"
shows "A = {}"
using assms
by (simp add: ordIso_iff_ordLeq card_of_empty1 card_of_empty2
ordLeq_Well_order_simp)
lemma card_of_empty_ordIso:
"|{}::'a set| =o |{}::'b set|"
using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
lemma card_of_image:
"|f ` A| <=o |A|"
proof(cases "A = {}", simp add: card_of_empty)
assume "A \ {}"
hence "f ` A \ {}" by auto
thus "|f ` A| \o |A|"
using card_of_ordLeq2[of "f ` A" A] by auto
qed
lemma surj_imp_ordLeq:
assumes "B \ f ` A"
shows "|B| \o |A|"
proof-
have "|B| <=o |f ` A|" using assms card_of_mono1 by auto
thus ?thesis using card_of_image ordLeq_transitive by blast
qed
lemma card_of_singl_ordLeq:
assumes "A \ {}"
shows "|{b}| \o |A|"
proof-
obtain a where *: "a \ A" using assms by auto
let ?h = "\ b'::'b. if b' = b then a else undefined"
have "inj_on ?h {b} \ ?h ` {b} \ A"
using * unfolding inj_on_def by auto
thus ?thesis unfolding card_of_ordLeq[symmetric] by (intro exI)
qed
corollary Card_order_singl_ordLeq:
"\Card_order r; Field r \ {}\ \ |{b}| \o r"
using card_of_singl_ordLeq[of "Field r" b]
card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast
lemma card_of_Pow: "|A|
using card_of_ordLess2[of "Pow A" A] Cantors_paradox[of A]
Pow_not_empty[of A] by auto
corollary Card_order_Pow:
"Card_order r \ r
using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast
lemma card_of_Plus1: "|A| \o |A <+> B|"
proof-
have "Inl ` A \ A <+> B" by auto
thus ?thesis using inj_Inl[of A] card_of_ordLeq by blast
qed
corollary Card_order_Plus1:
"Card_order r \ r \o |(Field r) <+> B|"
using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
lemma card_of_Plus2: "|B| \o |A <+> B|"
proof-
have "Inr ` B \ A <+> B" by auto
thus ?thesis using inj_Inr[of B] card_of_ordLeq by blast
qed
corollary Card_order_Plus2:
"Card_order r \ r \o |A <+> (Field r)|"
using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
lemma card_of_Plus_empty1: "|A| =o |A <+> {}|"
proof-
have "bij_betw Inl A (A <+> {})" unfolding bij_betw_def inj_on_def by auto
thus ?thesis using card_of_ordIso by auto
qed
lemma card_of_Plus_empty2: "|A| =o |{} <+> A|"
proof-
have "bij_betw Inr A ({} <+> A)" unfolding bij_betw_def inj_on_def by auto
thus ?thesis using card_of_ordIso by auto
qed
lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|"
proof-
let ?f = "\(c::'a + 'b). case c of Inl a \ Inr a
| Inr b \<Rightarrow> Inl b"
have "bij_betw ?f (A <+> B) (B <+> A)"
unfolding bij_betw_def inj_on_def by force
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Plus_assoc:
fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
shows "|(A <+> B) <+> C| =o |A <+> B <+> C|"
proof -
define f :: "('a + 'b) + 'c \ 'a + 'b + 'c"
where [abs_def]: "f k =
(case k of
Inl ab \<Rightarrow>
(case ab of
Inl a \<Rightarrow> Inl a
| Inr b \<Rightarrow> Inr (Inl b))
| Inr c \<Rightarrow> Inr (Inr c))"
for k
have "A <+> B <+> C \ f ` ((A <+> B) <+> C)"
proof
fix x assume x: "x \ A <+> B <+> C"
show "x \ f ` ((A <+> B) <+> C)"
proof(cases x)
case (Inl a)
hence "a \ A" "x = f (Inl (Inl a))"
using x unfolding f_def by auto
thus ?thesis by auto
next
case (Inr bc) note 1 = Inr show ?thesis
proof(cases bc)
case (Inl b)
hence "b \ B" "x = f (Inl (Inr b))"
using x 1 unfolding f_def by auto
thus ?thesis by auto
next
case (Inr c)
hence "c \ C" "x = f (Inr c)"
using x 1 unfolding f_def by auto
thus ?thesis by auto
qed
qed
qed
hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
unfolding bij_betw_def inj_on_def f_def by fastforce
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Plus_mono1:
assumes "|A| \o |B|"
shows "|A <+> C| \o |B <+> C|"
proof-
obtain f where 1: "inj_on f A \ f ` A \ B"
using assms card_of_ordLeq[of A] by fastforce
obtain g where g_def:
"g = (\d. case d of Inl a \ Inl(f a) | Inr (c::'c) \ Inr c)" by blast
have "inj_on g (A <+> C) \ g ` (A <+> C) \ (B <+> C)"
proof-
{fix d1 and d2 assume "d1 \ A <+> C \ d2 \ A <+> C" and
"g d1 = g d2"
hence "d1 = d2" using 1 unfolding inj_on_def g_def by force
}
moreover
{fix d assume "d \ A <+> C"
hence "g d \ B <+> C" using 1
by(cases d) (auto simp add: g_def)
}
ultimately show ?thesis unfolding inj_on_def by auto
qed
thus ?thesis using card_of_ordLeq by blast
qed
corollary ordLeq_Plus_mono1:
assumes "r \o r'"
shows "|(Field r) <+> C| \o |(Field r') <+> C|"
using assms card_of_mono2 card_of_Plus_mono1 by blast
lemma card_of_Plus_mono2:
assumes "|A| \o |B|"
shows "|C <+> A| \o |C <+> B|"
using assms card_of_Plus_mono1[of A B C]
card_of_Plus_commute[of C A] card_of_Plus_commute[of B C]
ordIso_ordLeq_trans[of "|C <+> A|"] ordLeq_ordIso_trans[of "|C <+> A|"]
by blast
corollary ordLeq_Plus_mono2:
assumes "r \o r'"
shows "|A <+> (Field r)| \o |A <+> (Field r')|"
using assms card_of_mono2 card_of_Plus_mono2 by blast
lemma card_of_Plus_mono:
assumes "|A| \o |B|" and "|C| \o |D|"
shows "|A <+> C| \o |B <+> D|"
using assms card_of_Plus_mono1[of A B C] card_of_Plus_mono2[of C D B]
ordLeq_transitive[of "|A <+> C|"] by blast
corollary ordLeq_Plus_mono:
assumes "r \o r'" and "p \o p'"
shows "|(Field r) <+> (Field p)| \o |(Field r') <+> (Field p')|"
using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast
lemma card_of_Plus_cong1:
assumes "|A| =o |B|"
shows "|A <+> C| =o |B <+> C|"
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1)
corollary ordIso_Plus_cong1:
assumes "r =o r'"
shows "|(Field r) <+> C| =o |(Field r') <+> C|"
using assms card_of_cong card_of_Plus_cong1 by blast
lemma card_of_Plus_cong2:
assumes "|A| =o |B|"
shows "|C <+> A| =o |C <+> B|"
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2)
corollary ordIso_Plus_cong2:
assumes "r =o r'"
shows "|A <+> (Field r)| =o |A <+> (Field r')|"
using assms card_of_cong card_of_Plus_cong2 by blast
lemma card_of_Plus_cong:
assumes "|A| =o |B|" and "|C| =o |D|"
shows "|A <+> C| =o |B <+> D|"
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono)
corollary ordIso_Plus_cong:
assumes "r =o r'" and "p =o p'"
shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|"
using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast
lemma card_of_Un_Plus_ordLeq:
"|A \ B| \o |A <+> B|"
proof-
let ?f = "\ c. if c \ A then Inl c else Inr c"
have "inj_on ?f (A \ B) \ ?f ` (A \ B) \ A <+> B"
unfolding inj_on_def by auto
thus ?thesis using card_of_ordLeq by blast
qed
lemma card_of_Times1:
assumes "A \ {}"
shows "|B| \o |B \ A|"
proof(cases "B = {}", simp add: card_of_empty)
assume *: "B \ {}"
have "fst `(B \ A) = B" using assms by auto
thus ?thesis using inj_on_iff_surj[of B "B \ A"]
card_of_ordLeq[of B "B \ A"] * by blast
qed
lemma card_of_Times_commute: "|A \ B| =o |B \ A|"
proof-
let ?f = "\(a::'a,b::'b). (b,a)"
have "bij_betw ?f (A \ B) (B \ A)"
unfolding bij_betw_def inj_on_def by auto
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Times2:
assumes "A \ {}" shows "|B| \o |A \ B|"
using assms card_of_Times1[of A B] card_of_Times_commute[of B A]
ordLeq_ordIso_trans by blast
corollary Card_order_Times1:
"\Card_order r; B \ {}\ \ r \o |(Field r) \ B|"
using card_of_Times1[of B] card_of_Field_ordIso
ordIso_ordLeq_trans ordIso_symmetric by blast
corollary Card_order_Times2:
"\Card_order r; A \ {}\ \ r \o |A \ (Field r)|"
using card_of_Times2[of A] card_of_Field_ordIso
ordIso_ordLeq_trans ordIso_symmetric by blast
lemma card_of_Times3: "|A| \o |A \ A|"
using card_of_Times1[of A]
by(cases "A = {}", simp add: card_of_empty, blast)
lemma card_of_Plus_Times_bool: "|A <+> A| =o |A \ (UNIV::bool set)|"
proof-
let ?f = "\c::'a + 'a. case c of Inl a \ (a,True)
|Inr a \<Rightarrow> (a,False)"
have "bij_betw ?f (A <+> A) (A \ (UNIV::bool set))"
proof-
{fix c1 and c2 assume "?f c1 = ?f c2"
hence "c1 = c2"
by(cases c1; cases c2) auto
}
moreover
{fix c assume "c \ A <+> A"
hence "?f c \ A \ (UNIV::bool set)"
by(cases c) auto
}
moreover
{fix a bl assume *: "(a,bl) \ A \ (UNIV::bool set)"
have "(a,bl) \ ?f ` ( A <+> A)"
proof(cases bl)
assume bl hence "?f(Inl a) = (a,bl)" by auto
thus ?thesis using * by force
next
assume "\ bl" hence "?f(Inr a) = (a,bl)" by auto
thus ?thesis using * by force
qed
}
ultimately show ?thesis unfolding bij_betw_def inj_on_def by auto
qed
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Times_mono1:
assumes "|A| \o |B|"
shows "|A \ C| \o |B \ C|"
proof-
obtain f where 1: "inj_on f A \ f ` A \ B"
using assms card_of_ordLeq[of A] by fastforce
obtain g where g_def:
"g = (\(a,c::'c). (f a,c))" by blast
have "inj_on g (A \ C) \ g ` (A \ C) \ (B \ C)"
using 1 unfolding inj_on_def using g_def by auto
thus ?thesis using card_of_ordLeq by blast
qed
corollary ordLeq_Times_mono1:
assumes "r \o r'"
shows "|(Field r) \ C| \o |(Field r') \ C|"
using assms card_of_mono2 card_of_Times_mono1 by blast
lemma card_of_Times_mono2:
assumes "|A| \o |B|"
shows "|C \ A| \o |C \ B|"
using assms card_of_Times_mono1[of A B C]
card_of_Times_commute[of C A] card_of_Times_commute[of B C]
ordIso_ordLeq_trans[of "|C \ A|"] ordLeq_ordIso_trans[of "|C \ A|"]
by blast
corollary ordLeq_Times_mono2:
assumes "r \o r'"
shows "|A \ (Field r)| \o |A \ (Field r')|"
using assms card_of_mono2 card_of_Times_mono2 by blast
lemma card_of_Sigma_mono1:
assumes "\i \ I. |A i| \o |B i|"
shows "|SIGMA i : I. A i| \o |SIGMA i : I. B i|"
proof-
have "\i. i \ I \ (\f. inj_on f (A i) \ f ` (A i) \ B i)"
using assms by (auto simp add: card_of_ordLeq)
with choice[of "\ i f. i \ I \ inj_on f (A i) \ f ` (A i) \ B i"]
obtain F where 1: "\i \ I. inj_on (F i) (A i) \ (F i) ` (A i) \ B i"
by atomize_elim (auto intro: bchoice)
obtain g where g_def: "g = (\(i,a::'b). (i,F i a))" by blast
have "inj_on g (Sigma I A) \ g ` (Sigma I A) \ (Sigma I B)"
using 1 unfolding inj_on_def using g_def by force
thus ?thesis using card_of_ordLeq by blast
qed
lemma card_of_UNION_Sigma:
"|\i \ I. A i| \o |SIGMA i : I. A i|"
using Ex_inj_on_UNION_Sigma [of A I] card_of_ordLeq by blast
lemma card_of_bool:
assumes "a1 \ a2"
shows "|UNIV::bool set| =o |{a1,a2}|"
proof-
let ?f = "\ bl. case bl of True \ a1 | False \ a2"
have "bij_betw ?f UNIV {a1,a2}"
proof-
{fix bl1 and bl2 assume "?f bl1 = ?f bl2"
hence "bl1 = bl2" using assms by (cases bl1, cases bl2) auto
}
moreover
{fix bl have "?f bl \ {a1,a2}" by (cases bl) auto
}
moreover
{fix a assume *: "a \ {a1,a2}"
have "a \ ?f ` UNIV"
proof(cases "a = a1")
assume "a = a1"
hence "?f True = a" by auto thus ?thesis by blast
next
assume "a \ a1" hence "a = a2" using * by auto
hence "?f False = a" by auto thus ?thesis by blast
qed
}
ultimately show ?thesis unfolding bij_betw_def inj_on_def by blast
qed
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Plus_Times_aux:
assumes A2: "a1 \ a2 \ {a1,a2} \ A" and
LEQ: "|A| \o |B|"
shows "|A <+> B| \o |A \ B|"
proof-
have 1: "|UNIV::bool set| \o |A|"
using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
ordIso_ordLeq_trans[of "|UNIV::bool set|"] by blast
(* *)
have "|A <+> B| \o |B <+> B|"
using LEQ card_of_Plus_mono1 by blast
moreover have "|B <+> B| =o |B \ (UNIV::bool set)|"
using card_of_Plus_Times_bool by blast
moreover have "|B \ (UNIV::bool set)| \o |B \ A|"
using 1 by (simp add: card_of_Times_mono2)
moreover have " |B \ A| =o |A \ B|"
using card_of_Times_commute by blast
ultimately show "|A <+> B| \o |A \ B|"
using ordLeq_ordIso_trans[of "|A <+> B|" "|B <+> B|" "|B \ (UNIV::bool set)|"]
ordLeq_transitive[of "|A <+> B|" "|B \ (UNIV::bool set)|" "|B \ A|"]
ordLeq_ordIso_trans[of "|A <+> B|" "|B \ A|" "|A \ B|"]
by blast
qed
lemma card_of_Plus_Times:
assumes A2: "a1 \ a2 \ {a1,a2} \ A" and
B2: "b1 \ b2 \ {b1,b2} \ B"
shows "|A <+> B| \o |A \ B|"
proof-
{assume "|A| \o |B|"
hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux)
}
moreover
{assume "|B| \o |A|"
hence "|B <+> A| \o |B \ A|"
using assms by (auto simp add: card_of_Plus_Times_aux)
hence ?thesis
using card_of_Plus_commute card_of_Times_commute
ordIso_ordLeq_trans ordLeq_ordIso_trans by blast
}
ultimately show ?thesis
using card_of_Well_order[of A] card_of_Well_order[of B]
ordLeq_total[of "|A|"] by blast
qed
lemma card_of_Times_Plus_distrib:
"|A \ (B <+> C)| =o |A \ B <+> A \ C|" (is "|?RHS| =o |?LHS|")
proof -
let ?f = "\(a, bc). case bc of Inl b \ Inl (a, b) | Inr c \ Inr (a, c)"
have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_ordLeq_finite:
assumes "|A| \o |B|" and "finite B"
shows "finite A"
using assms unfolding ordLeq_def
using embed_inj_on[of "|A|" "|B|"] embed_Field[of "|A|" "|B|"]
Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce
lemma card_of_ordLeq_infinite:
assumes "|A| \o |B|" and "\ finite A"
shows "\ finite B"
using assms card_of_ordLeq_finite by auto
lemma card_of_ordIso_finite:
assumes "|A| =o |B|"
shows "finite A = finite B"
using assms unfolding ordIso_def iso_def[abs_def]
by (auto simp: bij_betw_finite Field_card_of)
lemma card_of_ordIso_finite_Field:
assumes "Card_order r" and "r =o |A|"
shows "finite(Field r) = finite A"
using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast
subsection \<open>Cardinals versus set operations involving infinite sets\<close>
text\<open>Here we show that, for infinite sets, most set-theoretic constructions
do not increase the cardinality. The cornerstone for this is
theorem \<open>Card_order_Times_same_infinite\<close>, which states that self-product
does not increase cardinality -- the proof of this fact adapts a standard
set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
at page 47 in @{cite "card-book"}. Then everything else follows fairly easily.\<close>
lemma infinite_iff_card_of_nat:
"\ finite A \ ( |UNIV::nat set| \o |A| )"
unfolding infinite_iff_countable_subset card_of_ordLeq ..
text\<open>The next two results correspond to the ZF fact that all infinite cardinals are
limit ordinals:\<close>
lemma Card_order_infinite_not_under:
assumes CARD: "Card_order r" and INF: "\finite (Field r)"
shows "\ (\a. Field r = under r a)"
proof(auto)
have 0: "Well_order r \ wo_rel r \ Refl r"
using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
fix a assume *: "Field r = under r a"
show False
proof(cases "a \ Field r")
assume Case1: "a \ Field r"
hence "under r a = {}" unfolding Field_def under_def by auto
thus False using INF * by auto
next
let ?r' = "Restr r (underS r a)"
assume Case2: "a \ Field r"
hence 1: "under r a = underS r a \ {a} \ a \ underS r a"
using 0 Refl_under_underS[of r a] underS_notIn[of a r] by blast
have 2: "wo_rel.ofilter r (underS r a) \ underS r a < Field r"
using 0 wo_rel.underS_ofilter * 1 Case2 by fast
hence "?r' using 0 using ofilter_ordLess by blast
moreover
have "Field ?r' = underS r a \ Well_order ?r'"
using 2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
ultimately have "|underS r a| using ordLess_Field[of ?r'] by auto
moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
ultimately have "|underS r a|
using ordIso_symmetric ordLess_ordIso_trans by blast
moreover
{have "\f. bij_betw f (under r a) (underS r a)"
using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
hence "|under r a| =o |underS r a|" using card_of_ordIso by blast
}
ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
qed
qed
lemma infinite_Card_order_limit:
assumes r: "Card_order r" and "\finite (Field r)"
and a: "a \ Field r"
shows "\b \ Field r. a \ b \ (a,b) \ r"
proof-
have "Field r \ under r a"
using assms Card_order_infinite_not_under by blast
moreover have "under r a \ Field r"
using under_Field .
ultimately have "under r a < Field r" by blast
then obtain b where 1: "b \ Field r \ \ (b,a) \ r"
unfolding under_def by blast
moreover have ba: "b \ a"
using 1 r unfolding card_order_on_def well_order_on_def
linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
ultimately have "(a,b) \ r"
using a r unfolding card_order_on_def well_order_on_def linear_order_on_def
total_on_def by blast
thus ?thesis using 1 ba by auto
qed
theorem Card_order_Times_same_infinite:
assumes CO: "Card_order r" and INF: "\finite(Field r)"
shows "|Field r \ Field r| \o r"
proof-
obtain phi where phi_def:
"phi = (\r::'a rel. Card_order r \ \finite(Field r) \
\<not> |Field r \<times> Field r| \<le>o r )" by blast
have temp1: "\r. phi r \ Well_order r"
unfolding phi_def card_order_on_def by auto
have Ft: "\(\r. phi r)"
proof
assume "\r. phi r"
hence "{r. phi r} \ {} \ {r. phi r} \ {r. Well_order r}"
using temp1 by auto
then obtain r where 1: "phi r" and 2: "\r'. phi r' \ r \o r'" and
3: "Card_order r \ Well_order r"
using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast
let ?A = "Field r" let ?r' = "bsqr r"
have 4: "Well_order ?r' \ Field ?r' = ?A \ ?A \ |?A| =o r"
using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast
have 5: "Card_order |?A \ ?A| \ Well_order |?A \ ?A|"
using card_of_Card_order card_of_Well_order by blast
(* *)
have "r ?A|"
using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast
moreover have "|?A \ ?A| \o ?r'"
using card_of_least[of "?A \ ?A"] 4 by auto
ultimately have "r using ordLess_ordLeq_trans by auto
then obtain f where 6: "embed r ?r' f" and 7: "\ bij_betw f ?A (?A \ ?A)"
unfolding ordLess_def embedS_def[abs_def]
by (auto simp add: Field_bsqr)
let ?B = "f ` ?A"
have "|?A| =o |?B|"
using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast
hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast
(* *)
have "wo_rel.ofilter ?r' ?B"
using 6 embed_Field_ofilter 3 4 by blast
hence "wo_rel.ofilter ?r' ?B \ ?B \ ?A \ ?A \ ?B \ Field ?r'"
using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
hence temp2: "wo_rel.ofilter ?r' ?B \ ?B < ?A \ ?A"
using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
have "\ (\a. Field r = under r a)"
using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
then obtain A1 where temp3: "wo_rel.ofilter r A1 \ A1 < ?A" and 9: "?B \ A1 \ A1"
using temp2 3 bsqr_ofilter[of r ?B] by blast
hence "|?B| \o |A1 \ A1|" using card_of_mono1 by blast
hence 10: "r \o |A1 \ A1|" using 8 ordIso_ordLeq_trans by blast
let ?r1 = "Restr r A1"
have "?r1 using temp3 ofilter_ordLess 3 by blast
moreover
{have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast
hence "|A1| \o ?r1" using 3 Well_order_Restr card_of_least by blast
}
ultimately have 11: "|A1| using ordLeq_ordLess_trans by blast
(* *)
have "\ finite (Field r)" using 1 unfolding phi_def by simp
hence "\ finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
hence "\ finite A1" using 9 finite_cartesian_product finite_subset by blast
moreover have temp4: "Field |A1| = A1 \ Well_order |A1| \ Card_order |A1|"
using card_of_Card_order[of A1] card_of_Well_order[of A1]
by (simp add: Field_card_of)
moreover have "\ r \o | A1 |"
using temp4 11 3 using not_ordLeq_iff_ordLess by blast
ultimately have "\ finite(Field |A1| ) \ Card_order |A1| \ \ r \o | A1 |"
by (simp add: card_of_card_order_on)
hence "|Field |A1| \ Field |A1| | \o |A1|"
using 2 unfolding phi_def by blast
hence "|A1 \ A1 | \o |A1|" using temp4 by auto
hence "r \o |A1|" using 10 ordLeq_transitive by blast
thus False using 11 not_ordLess_ordLeq by auto
qed
thus ?thesis using assms unfolding phi_def by blast
qed
corollary card_of_Times_same_infinite:
assumes "\finite A"
shows "|A \ A| =o |A|"
proof-
let ?r = "|A|"
have "Field ?r = A \ Card_order ?r"
using Field_card_of card_of_Card_order[of A] by fastforce
hence "|A \ A| \o |A|"
using Card_order_Times_same_infinite[of ?r] assms by auto
thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast
qed
lemma card_of_Times_infinite:
assumes INF: "\finite A" and NE: "B \ {}" and LEQ: "|B| \o |A|"
shows "|A \ B| =o |A| \ |B \ A| =o |A|"
proof-
have "|A| \o |A \ B| \ |A| \o |B \ A|"
using assms by (simp add: card_of_Times1 card_of_Times2)
moreover
{have "|A \ B| \o |A \ A| \ |B \ A| \o |A \ A|"
using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast
moreover have "|A \ A| =o |A|" using INF card_of_Times_same_infinite by blast
ultimately have "|A \ B| \o |A| \ |B \ A| \o |A|"
using ordLeq_ordIso_trans[of "|A \ B|"] ordLeq_ordIso_trans[of "|B \ A|"] by auto
}
ultimately show ?thesis by (simp add: ordIso_iff_ordLeq)
qed
corollary Card_order_Times_infinite:
assumes INF: "\finite(Field r)" and CARD: "Card_order r" and
NE: "Field p \ {}" and LEQ: "p \o r"
shows "| (Field r) \ (Field p) | =o r \ | (Field p) \ (Field r) | =o r"
proof-
have "|Field r \ Field p| =o |Field r| \ |Field p \ Field r| =o |Field r|"
using assms by (simp add: card_of_Times_infinite card_of_mono2)
thus ?thesis
using assms card_of_Field_ordIso[of r]
ordIso_transitive[of "|Field r \ Field p|"]
ordIso_transitive[of _ "|Field r|"] by blast
qed
lemma card_of_Sigma_ordLeq_infinite:
assumes INF: "\finite B" and
LEQ_I: "|I| \o |B|" and LEQ: "\i \ I. |A i| \o |B|"
shows "|SIGMA i : I. A i| \o |B|"
proof(cases "I = {}", simp add: card_of_empty)
assume *: "I \ {}"
have "|SIGMA i : I. A i| \o |I \ B|"
using card_of_Sigma_mono1[OF LEQ] by blast
moreover have "|I \ B| =o |B|"
using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
ultimately show ?thesis using ordLeq_ordIso_trans by blast
qed
lemma card_of_Sigma_ordLeq_infinite_Field:
assumes INF: "\finite (Field r)" and r: "Card_order r" and
LEQ_I: "|I| \o r" and LEQ: "\i \ I. |A i| \o r"
shows "|SIGMA i : I. A i| \o r"
proof-
let ?B = "Field r"
have 1: "r =o |?B| \ |?B| =o r" using r card_of_Field_ordIso
ordIso_symmetric by blast
hence "|I| \o |?B|" "\i \ I. |A i| \o |?B|"
using LEQ_I LEQ ordLeq_ordIso_trans by blast+
hence "|SIGMA i : I. A i| \o |?B|" using INF LEQ
card_of_Sigma_ordLeq_infinite by blast
thus ?thesis using 1 ordLeq_ordIso_trans by blast
qed
lemma card_of_Times_ordLeq_infinite_Field:
"\\finite (Field r); |A| \o r; |B| \o r; Card_order r\
\<Longrightarrow> |A \<times> B| \<le>o r"
by(simp add: card_of_Sigma_ordLeq_infinite_Field)
lemma card_of_Times_infinite_simps:
"\\finite A; B \ {}; |B| \o |A|\ \ |A \ B| =o |A|"
"\\finite A; B \ {}; |B| \o |A|\ \ |A| =o |A \ B|"
"\\finite A; B \ {}; |B| \o |A|\ \ |B \ A| =o |A|"
"\\finite A; B \ {}; |B| \o |A|\ \ |A| =o |B \ A|"
by (auto simp add: card_of_Times_infinite ordIso_symmetric)
lemma card_of_UNION_ordLeq_infinite:
assumes INF: "\finite B" and
LEQ_I: "|I| \o |B|" and LEQ: "\i \ I. |A i| \o |B|"
shows "|\i \ I. A i| \o |B|"
proof(cases "I = {}", simp add: card_of_empty)
assume *: "I \ {}"
have "|\i \ I. A i| \o |SIGMA i : I. A i|"
using card_of_UNION_Sigma by blast
moreover have "|SIGMA i : I. A i| \o |B|"
using assms card_of_Sigma_ordLeq_infinite by blast
ultimately show ?thesis using ordLeq_transitive by blast
qed
corollary card_of_UNION_ordLeq_infinite_Field:
assumes INF: "\finite (Field r)" and r: "Card_order r" and
LEQ_I: "|I| \o r" and LEQ: "\i \ I. |A i| \o r"
shows "|\i \ I. A i| \o r"
proof-
let ?B = "Field r"
have 1: "r =o |?B| \ |?B| =o r" using r card_of_Field_ordIso
ordIso_symmetric by blast
hence "|I| \o |?B|" "\i \ I. |A i| \o |?B|"
using LEQ_I LEQ ordLeq_ordIso_trans by blast+
hence "|\i \ I. A i| \o |?B|" using INF LEQ
card_of_UNION_ordLeq_infinite by blast
thus ?thesis using 1 ordLeq_ordIso_trans by blast
qed
lemma card_of_Plus_infinite1:
assumes INF: "\finite A" and LEQ: "|B| \o |A|"
shows "|A <+> B| =o |A|"
proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
let ?Inl = "Inl::'a \ 'a + 'b" let ?Inr = "Inr::'b \ 'a + 'b"
assume *: "B \ {}"
then obtain b1 where 1: "b1 \ B" by blast
show ?thesis
proof(cases "B = {b1}")
assume Case1: "B = {b1}"
have 2: "bij_betw ?Inl A ((?Inl ` A))"
unfolding bij_betw_def inj_on_def by auto
hence 3: "\finite (?Inl ` A)"
using INF bij_betw_finite[of ?Inl A] by blast
let ?A' = "?Inl ` A \ {?Inr b1}"
obtain g where "bij_betw g (?Inl ` A) ?A'"
using 3 infinite_imp_bij_betw2[of "?Inl ` A"] by auto
moreover have "?A' = A <+> B" using Case1 by blast
ultimately have "bij_betw g (?Inl ` A) (A <+> B)" by simp
hence "bij_betw (g \ ?Inl) A (A <+> B)"
using 2 by (auto simp add: bij_betw_trans)
thus ?thesis using card_of_ordIso ordIso_symmetric by blast
next
assume Case2: "B \ {b1}"
with * 1 obtain b2 where 3: "b1 \ b2 \ {b1,b2} \ B" by fastforce
obtain f where "inj_on f B \ f ` B \ A"
using LEQ card_of_ordLeq[of B] by fastforce
with 3 have "f b1 \ f b2 \ {f b1, f b2} \ A"
unfolding inj_on_def by auto
with 3 have "|A <+> B| \o |A \ B|"
by (auto simp add: card_of_Plus_Times)
moreover have "|A \ B| =o |A|"
using assms * by (simp add: card_of_Times_infinite_simps)
ultimately have "|A <+> B| \o |A|" using ordLeq_ordIso_trans by blast
thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
qed
qed
lemma card_of_Plus_infinite2:
assumes INF: "\finite A" and LEQ: "|B| \o |A|"
shows "|B <+> A| =o |A|"
using assms card_of_Plus_commute card_of_Plus_infinite1
ordIso_equivalence by blast
lemma card_of_Plus_infinite:
assumes INF: "\finite A" and LEQ: "|B| \o |A|"
shows "|A <+> B| =o |A| \ |B <+> A| =o |A|"
using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
corollary Card_order_Plus_infinite:
assumes INF: "\finite(Field r)" and CARD: "Card_order r" and
LEQ: "p \o r"
shows "| (Field r) <+> (Field p) | =o r \ | (Field p) <+> (Field r) | =o r"
proof-
have "| Field r <+> Field p | =o | Field r | \
| Field p <+> Field r | =o | Field r |"
using assms by (simp add: card_of_Plus_infinite card_of_mono2)
thus ?thesis
using assms card_of_Field_ordIso[of r]
ordIso_transitive[of "|Field r <+> Field p|"]
ordIso_transitive[of _ "|Field r|"] by blast
qed
subsection \<open>The cardinal $\omega$ and the finite cardinals\<close>
text\<open>The cardinal $\omega$, of natural numbers, shall be the standard non-strict
order relation on
\<open>nat\<close>, that we abbreviate by \<open>natLeq\<close>. The finite cardinals
shall be the restrictions of these relations to the numbers smaller than
fixed numbers \<open>n\<close>, that we abbreviate by \<open>natLeq_on n\<close>.\<close>
definition "(natLeq::(nat * nat) set) \ {(x,y). x \ y}"
definition "(natLess::(nat * nat) set) \ {(x,y). x < y}"
abbreviation natLeq_on :: "nat \ (nat * nat) set"
where "natLeq_on n \ {(x,y). x < n \ y < n \ x \ y}"
lemma infinite_cartesian_product:
assumes "\finite A" "\finite B"
shows "\finite (A \ B)"
proof
assume "finite (A \ B)"
from assms(1) have "A \ {}" by auto
with \<open>finite (A \<times> B)\<close> have "finite B" using finite_cartesian_productD2 by auto
with assms(2) show False by simp
qed
subsubsection \<open>First as well-orders\<close>
lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
by(unfold Field_def natLeq_def, auto)
lemma natLeq_Refl: "Refl natLeq"
unfolding refl_on_def Field_def natLeq_def by auto
lemma natLeq_trans: "trans natLeq"
unfolding trans_def natLeq_def by auto
lemma natLeq_Preorder: "Preorder natLeq"
unfolding preorder_on_def
by (auto simp add: natLeq_Refl natLeq_trans)
lemma natLeq_antisym: "antisym natLeq"
unfolding antisym_def natLeq_def by auto
lemma natLeq_Partial_order: "Partial_order natLeq"
unfolding partial_order_on_def
by (auto simp add: natLeq_Preorder natLeq_antisym)
lemma natLeq_Total: "Total natLeq"
unfolding total_on_def natLeq_def by auto
lemma natLeq_Linear_order: "Linear_order natLeq"
unfolding linear_order_on_def
by (auto simp add: natLeq_Partial_order natLeq_Total)
lemma natLeq_natLess_Id: "natLess = natLeq - Id"
unfolding natLeq_def natLess_def by auto
lemma natLeq_Well_order: "Well_order natLeq"
unfolding well_order_on_def
using natLeq_Linear_order wf_less natLeq_natLess_Id natLeq_def natLess_def by auto
lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
unfolding Field_def by auto
lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
unfolding underS_def natLeq_def by auto
lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
unfolding natLeq_def by force
lemma Restr_natLeq2:
"Restr natLeq (underS natLeq n) = natLeq_on n"
by (auto simp add: Restr_natLeq natLeq_underS_less)
lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
using Restr_natLeq[of n] natLeq_Well_order
Well_order_Restr[of natLeq "{x. x < n}"] by auto
corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)"
using natLeq_on_Well_order Field_natLeq_on by auto
lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)"
unfolding wo_rel_def using natLeq_on_Well_order .
subsubsection \<open>Then as cardinals\<close>
lemma natLeq_Card_order: "Card_order natLeq"
proof(auto simp add: natLeq_Well_order
Card_order_iff_Restr_underS Restr_natLeq2, simp add: Field_natLeq)
fix n have "finite(Field (natLeq_on n))" by (auto simp: Field_def)
moreover have "\finite(UNIV::nat set)" by auto
ultimately show "natLeq_on n
using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
Field_card_of[of "UNIV::nat set"]
card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order[of n] by auto
qed
corollary card_of_Field_natLeq:
"|Field natLeq| =o natLeq"
using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq]
ordIso_symmetric[of natLeq] by blast
corollary card_of_nat:
"|UNIV::nat set| =o natLeq"
using Field_natLeq card_of_Field_natLeq by auto
corollary infinite_iff_natLeq_ordLeq:
"\finite A = ( natLeq \o |A| )"
using infinite_iff_card_of_nat[of A] card_of_nat
ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
corollary finite_iff_ordLess_natLeq:
"finite A = ( |A|
using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
card_of_Well_order natLeq_Well_order by blast
subsection \<open>The successor of a cardinal\<close>
text\<open>First we define \<open>isCardSuc r r'\<close>, the notion of \<open>r'\<close>
being a successor cardinal of \<open>r\<close>. Although the definition does
not require \<open>r\<close> to be a cardinal, only this case will be meaningful.\<close>
definition isCardSuc :: "'a rel \ 'a set rel \ bool"
where
"isCardSuc r r' \
Card_order r' \ r
(\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
text\<open>Now we introduce the cardinal-successor operator \<open>cardSuc\<close>,
by picking {\em some} cardinal-order relation fulfilling \<open>isCardSuc\<close>.
Again, the picked item shall be proved unique up to order-isomorphism.\<close>
definition cardSuc :: "'a rel \ 'a set rel"
where
"cardSuc r \ SOME r'. isCardSuc r r'"
lemma exists_minim_Card_order:
"\R \ {}; \r \ R. Card_order r\ \ \r \ R. \r' \ R. r \o r'"
unfolding card_order_on_def using exists_minim_Well_order by blast
lemma exists_isCardSuc:
assumes "Card_order r"
shows "\r'. isCardSuc r r'"
proof-
let ?R = "{(r'::'a set rel). Card_order r' \ r
have "|Pow(Field r)| \ ?R \ (\r \ ?R. Card_order r)" using assms
by (simp add: card_of_Card_order Card_order_Pow)
then obtain r where "r \ ?R \ (\r' \ ?R. r \o r')"
using exists_minim_Card_order[of ?R] by blast
thus ?thesis unfolding isCardSuc_def by auto
qed
lemma cardSuc_isCardSuc:
assumes "Card_order r"
shows "isCardSuc r (cardSuc r)"
unfolding cardSuc_def using assms
by (simp add: exists_isCardSuc someI_ex)
lemma cardSuc_Card_order:
"Card_order r \ Card_order(cardSuc r)"
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
lemma cardSuc_greater:
"Card_order r \ r
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
lemma cardSuc_ordLeq:
"Card_order r \ r \o cardSuc r"
using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
text\<open>The minimality property of \<open>cardSuc\<close> originally present in its definition
is local to the type \<open>'a set rel\<close>, i.e., that of \<open>cardSuc r\<close>:\<close>
lemma cardSuc_least_aux:
"\Card_order (r::'a rel); Card_order (r'::'a set rel); r \ cardSuc r \o r'"
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
text\<open>But from this we can infer general minimality:\<close>
lemma cardSuc_least:
assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"
shows "cardSuc r \o r'"
proof-
let ?p = "cardSuc r"
have 0: "Well_order ?p \ Well_order r'"
using assms cardSuc_Card_order unfolding card_order_on_def by blast
{assume "r'
then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' \ r''
using internalize_ordLess[of r' ?p] by blast
(* *)
have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast
moreover have "r using LESS 2 ordLess_ordIso_trans by blast
ultimately have "?p \o r''" using cardSuc_least_aux CARD by blast
hence False using 2 not_ordLess_ordLeq by blast
}
thus ?thesis using 0 ordLess_or_ordLeq by blast
qed
lemma cardSuc_ordLess_ordLeq:
assumes CARD: "Card_order r" and CARD': "Card_order r'"
shows "(r o r')"
proof(auto simp add: assms cardSuc_least)
assume "cardSuc r \o r'"
thus "r using assms cardSuc_greater ordLess_ordLeq_trans by blast
qed
lemma cardSuc_ordLeq_ordLess:
assumes CARD: "Card_order r" and CARD': "Card_order r'"
shows "(r' o r)"
proof-
have "Well_order r \ Well_order r'"
using assms unfolding card_order_on_def by auto
moreover have "Well_order(cardSuc r)"
using assms cardSuc_Card_order card_order_on_def by blast
ultimately show ?thesis
using assms cardSuc_ordLess_ordLeq[of r r']
not_ordLeq_iff_ordLess[of r r'] not_ordLeq_iff_ordLess[of r' "cardSuc r"] by blast
qed
lemma cardSuc_mono_ordLeq:
assumes CARD: "Card_order r" and CARD': "Card_order r'"
shows "(cardSuc r \o cardSuc r') = (r \o r')"
using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast
lemma cardSuc_invar_ordIso:
assumes CARD: "Card_order r" and CARD': "Card_order r'"
shows "(cardSuc r =o cardSuc r') = (r =o r')"
proof-
have 0: "Well_order r \ Well_order r' \ Well_order(cardSuc r) \ Well_order(cardSuc r')"
using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order)
thus ?thesis
using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq
using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast
qed
lemma card_of_cardSuc_finite:
"finite(Field(cardSuc |A| )) = finite A"
proof
assume *: "finite (Field (cardSuc |A| ))"
have 0: "|Field(cardSuc |A| )| =o cardSuc |A|"
using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
hence "|A| \o |Field(cardSuc |A| )|"
using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric
ordLeq_ordIso_trans by blast
thus "finite A" using * card_of_ordLeq_finite by blast
next
assume "finite A"
then have "finite ( Field |Pow A| )" unfolding Field_card_of by simp
then show "finite (Field (cardSuc |A| ))"
proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
show "cardSuc |A| \o |Pow A|"
by (rule iffD1[OF cardSuc_ordLess_ordLeq card_of_Pow]) (simp_all add: card_of_Card_order)
qed
qed
lemma cardSuc_finite:
assumes "Card_order r"
shows "finite (Field (cardSuc r)) = finite (Field r)"
proof-
let ?A = "Field r"
have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso)
hence "cardSuc |?A| =o cardSuc r" using assms
by (simp add: card_of_Card_order cardSuc_invar_ordIso)
moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|"
by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order)
moreover
{have "|Field (cardSuc r) | =o cardSuc r"
using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order)
hence "cardSuc r =o |Field (cardSuc r) |"
using ordIso_symmetric by blast
}
ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |"
using ordIso_transitive by blast
hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))"
using card_of_ordIso_finite by blast
thus ?thesis by (simp only: card_of_cardSuc_finite)
qed
lemma card_of_Plus_ordLess_infinite:
assumes INF: "\finite C" and
LESS1: "|A| and LESS2: "|B|
shows "|A <+> B|
proof(cases "A = {} \ B = {}")
assume Case1: "A = {} \ B = {}"
hence "|A| =o |A <+> B| \ |B| =o |A <+> B|"
using card_of_Plus_empty1 card_of_Plus_empty2 by blast
hence "|A <+> B| =o |A| \ |A <+> B| =o |B|"
using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast
thus ?thesis using LESS1 LESS2
ordIso_ordLess_trans[of "|A <+> B|" "|A|"]
ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast
next
assume Case2: "\(A = {} \ B = {})"
{assume *: "|C| \o |A <+> B|"
hence "\finite (A <+> B)" using INF card_of_ordLeq_finite by blast
hence 1: "\finite A \ \finite B" using finite_Plus by blast
{assume Case21: "|A| \o |B|"
hence "\finite B" using 1 card_of_ordLeq_finite by blast
hence "|A <+> B| =o |B|" using Case2 Case21
by (auto simp add: card_of_Plus_infinite)
hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
}
moreover
{assume Case22: "|B| \o |A|"
hence "\finite A" using 1 card_of_ordLeq_finite by blast
hence "|A <+> B| =o |A|" using Case2 Case22
by (auto simp add: card_of_Plus_infinite)
hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
}
ultimately have False using ordLeq_total card_of_Well_order[of A]
card_of_Well_order[of B] by blast
}
thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"]
card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto
qed
lemma card_of_Plus_ordLess_infinite_Field:
assumes INF: "\finite (Field r)" and r: "Card_order r" and
LESS1: "|A| and LESS2: "|B|
shows "|A <+> B|
proof-
let ?C = "Field r"
have 1: "r =o |?C| \ |?C| =o r" using r card_of_Field_ordIso
ordIso_symmetric by blast
hence "|A| "|B|
using LESS1 LESS2 ordLess_ordIso_trans by blast+
hence "|A <+> B| using INF
card_of_Plus_ordLess_infinite by blast
thus ?thesis using 1 ordLess_ordIso_trans by blast
qed
lemma card_of_Plus_ordLeq_infinite_Field:
assumes r: "\finite (Field r)" and A: "|A| \o r" and B: "|B| \o r"
and c: "Card_order r"
shows "|A <+> B| \o r"
proof-
let ?r' = "cardSuc r"
have "Card_order ?r' \ \finite (Field ?r')" using assms
by (simp add: cardSuc_Card_order cardSuc_finite)
moreover have "|A| and "|B| using A B c
by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
ultimately have "|A <+> B|
using card_of_Plus_ordLess_infinite_Field by blast
thus ?thesis using c r
by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
qed
lemma card_of_Un_ordLeq_infinite_Field:
assumes C: "\finite (Field r)" and A: "|A| \o r" and B: "|B| \o r"
and "Card_order r"
shows "|A Un B| \o r"
using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
ordLeq_transitive by fast
subsection \<open>Regular cardinals\<close>
definition cofinal where
"cofinal A r \
\<forall>a \<in> Field r. \<exists>b \<in> A. a \<noteq> b \<and> (a,b) \<in> r"
definition regularCard where
"regularCard r \
\<forall>K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
definition relChain where
"relChain r As \
\<forall>i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
lemma regularCard_UNION:
assumes r: "Card_order r" "regularCard r"
and As: "relChain r As"
and Bsub: "B \ (\i \ Field r. As i)"
and cardB: "|B|
shows "\i \ Field r. B \ As i"
proof-
let ?phi = "\b j. j \ Field r \ b \ As j"
have "\b\B. \j. ?phi b j" using Bsub by blast
then obtain f where f: "\b. b \ B \ ?phi b (f b)"
using bchoice[of B ?phi] by blast
let ?K = "f ` B"
{assume 1: "\i. i \ Field r \ \ B \ As i"
have 2: "cofinal ?K r"
unfolding cofinal_def proof auto
fix i assume i: "i \ Field r"
with 1 obtain b where b: "b \ B \ b \ As i" by blast
hence "i \ f b \ \ (f b,i) \ r"
using As f unfolding relChain_def by auto
hence "i \ f b \ (i, f b) \ r" using r
unfolding card_order_on_def well_order_on_def linear_order_on_def
total_on_def using i f b by auto
with b show "\b\B. i \ f b \ (i, f b) \ r" by blast
qed
moreover have "?K \ Field r" using f by blast
ultimately have "|?K| =o r" using 2 r unfolding regularCard_def by blast
moreover
{
have "|?K| <=o |B|" using card_of_image .
hence "|?K| using cardB ordLeq_ordLess_trans by blast
}
ultimately have False using not_ordLess_ordIso by blast
}
thus ?thesis by blast
qed
lemma infinite_cardSuc_regularCard:
assumes r_inf: "\finite (Field r)" and r_card: "Card_order r"
shows "regularCard (cardSuc r)"
proof-
let ?r' = "cardSuc r"
have r': "Card_order ?r'"
"!! p. Card_order p \ (p \o r) = (p
using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)
show ?thesis
unfolding regularCard_def proof auto
fix K assume 1: "K \ Field ?r'" and 2: "cofinal K ?r'"
hence "|K| \o |Field ?r'|" by (simp only: card_of_mono1)
also have 22: "|Field ?r'| =o ?r'"
using r' by (simp add: card_of_Field_ordIso[of ?r'])
finally have "|K| \o ?r'" .
moreover
{let ?L = "\ j \ K. underS ?r' j"
let ?J = "Field r"
have rJ: "r =o |?J|"
using r_card card_of_Field_ordIso ordIso_symmetric by blast
assume "|K|
hence "|K| <=o r" using r' card_of_Card_order[of K] by blast
hence "|K| \o |?J|" using rJ ordLeq_ordIso_trans by blast
moreover
{have "\j\K. |underS ?r' j|
using r' 1 by (auto simp: card_of_underS)
hence "\j\K. |underS ?r' j| \o r"
using r' card_of_Card_order by blast
hence "\j\K. |underS ?r' j| \o |?J|"
using rJ ordLeq_ordIso_trans by blast
}
ultimately have "|?L| \o |?J|"
using r_inf card_of_UNION_ordLeq_infinite by blast
hence "|?L| \o r" using rJ ordIso_symmetric ordLeq_ordIso_trans by blast
hence "|?L| using r' card_of_Card_order by blast
moreover
{
have "Field ?r' \ ?L"
using 2 unfolding underS_def cofinal_def by auto
hence "|Field ?r'| \o |?L|" by (simp add: card_of_mono1)
hence "?r' \o |?L|"
using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
}
ultimately have "|?L| using ordLess_ordLeq_trans by blast
hence False using ordLess_irreflexive by blast
}
ultimately show "|K| =o ?r'"
unfolding ordLeq_iff_ordLess_or_ordIso by blast
qed
qed
lemma cardSuc_UNION:
assumes r: "Card_order r" and "\finite (Field r)"
and As: "relChain (cardSuc r) As"
and Bsub: "B \ (\ i \ Field (cardSuc r). As i)"
and cardB: "|B| <=o r"
shows "\i \ Field (cardSuc r). B \ As i"
proof-
let ?r' = "cardSuc r"
have "Card_order ?r' \ |B|
using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order
card_of_Card_order by blast
moreover have "regularCard ?r'"
using assms by(simp add: infinite_cardSuc_regularCard)
ultimately show ?thesis
using As Bsub cardB regularCard_UNION by blast
qed
subsection \<open>Others\<close>
lemma card_of_Func_Times:
"|Func (A \ B) C| =o |Func A (Func B C)|"
unfolding card_of_ordIso[symmetric]
using bij_betw_curr by blast
lemma card_of_Pow_Func:
"|Pow A| =o |Func A (UNIV::bool set)|"
proof-
define F where [abs_def]: "F A' a =
(if a \<in> A then (if a \<in> A' then True else False) else undefined)" for A' a
have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
fix A1 A2 assume "A1 \ Pow A" "A2 \ Pow A" "F A1 = F A2"
thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: if_split_asm)
next
show "F ` Pow A = Func A UNIV"
proof safe
fix f assume f: "f \ Func A (UNIV::bool set)"
show "f \ F ` Pow A" unfolding image_def mem_Collect_eq proof(intro bexI)
let ?A1 = "{a \ A. f a = True}"
show "f = F ?A1"
unfolding F_def apply(rule ext)
using f unfolding Func_def mem_Collect_eq by auto
qed auto
qed(unfold Func_def mem_Collect_eq F_def, auto)
qed
thus ?thesis unfolding card_of_ordIso[symmetric] by blast
qed
lemma card_of_Func_UNIV:
"|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \ 'b. range f \ B}|"
apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI)
let ?F = "\ f (a::'a). ((f a)::'b)"
show "bij_betw ?F {f. range f \ B} (Func UNIV B)"
unfolding bij_betw_def inj_on_def proof safe
fix h :: "'a \ 'b" assume h: "h \ Func UNIV B"
hence "\ a. \ b. h a = b" unfolding Func_def by auto
then obtain f where f: "\ a. h a = f a" by blast
hence "range f \ B" using h unfolding Func_def by auto
thus "h \ (\f a. f a) ` {f. range f \ B}" using f by auto
qed(unfold Func_def fun_eq_iff, auto)
qed
lemma Func_Times_Range:
"|Func A (B \ C)| =o |Func A B \ Func A C|" (is "|?LHS| =o |?RHS|")
proof -
let ?F = "\fg. (\x. if x \ A then fst (fg x) else undefined,
\<lambda>x. if x \<in> A then snd (fg x) else undefined)"
let ?G = "\(f, g) x. if x \ A then (f x, g x) else undefined"
have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
proof (intro conjI impI ballI equalityI subsetI)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.254 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.
|
|
|
|
|
|
