single_cone:
"|{x}| =o cone"
-
let ?f = "λx. ()"
have "bij_betw ?f {x} {()}" unfolding bij_betw_def by auto
thus ?thesis unfolding cone_def using card_of_ordIso by blast
cone_Cnotzero: "Cnotzero cone"
by (simp add: cone_not_czero Card_order_cone)
cone_ordLeq_ctwo: "cone ≤x. floor (real_of_int (f x))) at_bot F"
unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto
csum_czero1: "Card_order r ==> r +c czero =o r"
unfolding czero_def csum_def Field_card_of
by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty1] card_of_Field_ordIso])
csum_czero2: "Card_order r ==> czero +c r =o r"
unfolding czero_def csum_def Field_card_of
by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty2] card_of_Field_ordIso])
card_of_Times_singleton:
fixes A :: "'a set"
shows "|A ×
-
define f :: "'a × 'b → 'a" where "f = (λ(a, b). a)"
have "A ⊆ f ` (A × {x})" unfolding f_def by (auto simp: image_iff)
hence "bij_betw f (A × {x}) A" unfolding bij_betw_def inj_on_def f_def by fastforce
thus ?thesis using card_of_ordIso by blast
cprod_assoc: "(r *c s) *c t =o r *c s *c t"
unfolding cprod_def Field_card_of by (rule card_of_Times_assoc)
Cnotzero_cexp:
assumes "Cnotzero q"
shows "Cnotzero (q ^c r)"
-
have "Field q ≠ {}"
by (metis Card_order_iff_ordIso_card_of assms(1) czero_def)
then show ?thesis
by (simp add: card_of_ordIso_czero_iff_empty cexp_def)
Cinfinite_ctwo_cexp:
"Cinfinite r ==> Cinfinite (ctwo ^c r)"
unfolding ctwo_def cexp_def cinfinite_def Field_card_of
by (rule conjI, rule infinite_Func, auto)
cone_ordLeq_iff_Field:
assumes "cone ≤o r"
shows "Field r ≠ {}"
by (metis assms card_of_empty3 card_of_mono2 cone_Cnotzero czeroI)
cone_ordLeq_cexp:"cone≤ cone ≤
by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field)
Card_order_czero: "Card_order czero"
by (simp only: card_of_Card_order czero_def)
cexp_mono2'':
assumes 2: "p2 ≤o r2"
and n1: "Cnotzero q"
and n2: "Card_order p2"
shows "q ^c p2 ≤o q ^c r2"
(cases "p2 =o (czero :: 'a rel)")
case True
hence "q ^c p2 =o q ^c (czero :: 'a rel)" using n1 n2 cexp_cong2 Card_order_czero by blast
also have "q ^c (czero :: 'a rel) =o cone" using cexp_czero by blast
also have "cone ≤o q ^c r2" using cone_ordLeq_cexp cone_ordLeq_Cnotzero n1 by blast
finally show ?thesis .
case False thus ?thesis using assms cexp_mono2' czeroI by metis
ssumes "filterlim (λx. f x - c) (at_right 0) F"
Cinfinite_ordLess_cexp:
assumes r: "Cinfinite r"
shows "r <o r ^c r"
-
have "r <o ctwo ^c r" using r by (simp only: ordLess_ctwo_cexp)
also have "ctwo ^c r ≤o r ^c r"
by (rule cexp_mono1[OF ctwo_ordLeq_Cinfinite]) (auto simp: r ctwo_not_czero Card_order_ctwo)
finally show ?thesis .
infinite_ordLeq_cexp:
assumes "Cinfinite r"
shows "r ≤o r ^c r"
by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[roof -
czero_cexp: "Cnotzero r ==> czero ^c r =o czero"
by (metis Cnotzero_imp_not_empty cexp_def czero_def card_of_empty_ordIso Field_card_of Func_is_emp)
Func_singleton:
fixes x :: 'b and A :: "'a set"
shows "|Func A {x}| =o |{x}|"
(rule ordIso_symmetric)
define f where [abs_def]: "f y a = (if y = x ∧ a ∈ A then x else undefined)" for y a
have "Func A {x} ⊆ f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff)
hence "bij_betw f {x} (Func A {x})"
unfolding bij_betw_def inj_on_def f_def Func_def by (auto split: if_split_asm)
thus "|{x}| =o |Func A {x}|" using card_of_ordIso by blast
cone_cexp: "cone ^c r =o cone"
unfolding cexp_def cone_def Field_card_of by (rule Func_singleton)
card_of_Func_squared:
fixes A :: "'a set"
shows "|Func (UNIV :: bool set) A| =o |A × A|"
(rule ordIso_symmetric)
define f where "f = (λ(x::'a,y) b. if A = {} then undefined else if b then x else y)"
have "Func (UNIV :: bool set) A ⊆ hav "filterma (λx. f x - c) F ≤ at_right 0" by (simp add: filterlim_def)
by (auto simp: image_iff fun_eq_iff split: option.splits if_split_asm) blast
hence "bij_betw f (A × A) (Func (UNIV :: bool set) A)"
unfolding bij_betw_def inj_on_def f_def Func_def by (auto simp: fun_eq_iff)
thus "|A × A| =o |Func (UNIV :: bool set) A|" using card_of_ordIso by blast
cexp_ctwo: "r ^c ctwo =o r *c r"
unfolding cexp_def ctwo_def cprod_def Field_card_of by (rule card_of_Func_squared)
card_of_Func_Plus:
fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
shows "|Func (A 🚫
(rule ordIso_symmetric)
define f where "f = (λ(g :: 'a => 'c, hubsection ‹
define f' where "f' = (λ(f :: ('a + 'b) → 'c). (λa. f (Inl a), λb. f (Inr b)))"
have "f ` (Func A C × Func B C) ⊆ Func (A 🚫
unfolding Func_def f_def by (force split: sum.splits)
moreover have "f' ` Func (A 🚫REAL_ASYMP_ True"
moreover have "∀a ∈ Func A C × Func B C. f' (f a) = a" unfolding f'_def f_def Func_def by auto
moreover have "∀a' ∈
by (auto split: sum.splits)
ultimately have "bij_betw f (Func A C × Func B C) (Func (A 🚫
by (intro bij_betw_byWitness[of _ f' f])
thus "|Func A C × Func B C| =o |Func (A 🚫
cexp_csum: "r ^c (s +c t) =o r ^c s *c r ^c t"
unfolding cexp_def cprod_def csum_def Field_card_of by (rule card_of_Func_Plus)
‹Powerset›
cpow where "cpow r = |Pow (Field r)|"
card_order_cpow: "card_order r ==> card_order (cpow r)"
by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on)
cpow_greater_eq: "Card_order r ==> r ≤o cpow r"
by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow)
Cinfinite_cpow: "Cinfinite r ==> Cinfinite (cpow r)"
unfolding cpow_def cinfinite_def by simp
Card_order_cpow: "Card_order (cpow r)"
unfolding cpow_def by (rule card_of_Card_order)
cardSuc_ordLeq_cpow: "Card_order r ==> cardSuc r ≤o cpow r"
unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order)
cpow_cexp_ctwo: "cpow r =o ctwo ^c r"
unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
‹Inverse image›
vimage_ordLeq:
assumes "|A| ≤o k" and "∀ a ∈ A. |vimage f {a}| ≤o k" and "Cinfinite k"
shows "|vimage f A| ≤o k"
-
have "vimage f A = (∪a ∈ A. vimage f {a})" by auto
also have "|∪a ∈ A. vimage f {a}| ≤o k"
using UNION_Cinfinite_bound[OF assms] .
finally show ?thesis .
‹Maximum›
cmax where
"cmax r s =
(if cinfinite r ∨ cinfinite s then czero +c r +c s
else natLeq_on (max (card (Field r)) (card (Field s))) +c czero)"
cmax_com: "cmax r s =o cmax s r"
unfolding cmax_def
by (auto simp: max.commute intro: csum_cong2[OF csum_com] csum_cong2[OF czero_ordIso])
cmax1:
assumes "Card_order r" "Card_order s" "s ≤o r"
shows "cmax r s =o r"
unfolding cmax_def
(split if_splits, intro conjI impI)
assume "cinfinite r ∨ cinfinite s"
hence Cinf: "Cinfinite r" using assms(1,3) by (metis cinfinite_mono)
have "czero +c r +c s =o r +c s" by (rule csum_czero2[OF Card_order_csum])
also have "r +c s =o r" by (rule csum_absorb1[OF Cinf assms(3)])
finally show "czero +c r +c s =o r" .
assume "¬ (cinfinite r ∨ cinfinite s)"
hence fin: "finite (Field r)" and "finite (Field s)" unfolding cinfinite_def by simp_all
moreover
{ from assms(2) have "|Field s| =o s" by (rule card_of_Field_ordIso)
also from assms(3) have "s ≤o r" .
also from assms(1) have "r =o |Field r|" by (rule ordIso_symmetric[OF card_of_Field_ordIso])
finally have "|Field s| ≤o |Field r|" .
}
ultimately have "card (Field s) ≤ card (Field r)" by (subst sym[OF finite_card_of_iff_card2])
hence "max (card (Field r)) (card (Field s)) = card (Field r)" by (rule max_absorb1)
hence "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =
natLeq_on (card (Field r)) +c czero" by simp
also have "… =o natLeq_on (card (Field r))" by (rule csum_czero1[OF natLeq_on_Card_order])
also have "natLeq_on (card (Field r)) =o |Field r|"
by (rule ordIso_symmetric[OF finite_imp_card_of_natLeq_on[OF fin]])
also from assms(1) have "|Field r| =o r" by (rule card_of_Field_ordIso)
finally show "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =o r" .
cmax2:
assumes "Card_order r" "Card_order s" "r ≤o s"
shows "cmax r s =o s"
by (metis assms cmax1 cmax_com ordIso_transitive)
fixes r s
assumes r: "Cinfinite r"
and s: "Cinfinite s"
cmax_csum: "cmax r s =o r +c s"
by (simp add: Card_order_csum cmax_def csum_czero2 r)
cmax_cprod: "cmax r s =o r *c s"
(cases "r ≤o s")
case True
hence "cmax r s =o s" by (metis cmax2 r s)
also have "s =o r *c s" by (metis Cinfinite_Cnotzero True cprod_infinite2' ordIso_symmetric r s)
finally show ?thesis .
case False
hence "s ≤o r" by (metis ordLeq_total r s card_order_on_def)
hence "cmax r s =o r" by (metis cmax1 r s)
also have "r =o r *c s" by (metis Cinfinite_Cnotzero ‹s ≤o r› cprod_infinite1' ordIso_symmetric r s)
finally show ?thesis .
Card_order_cmax:
assumes r: "Card_order r" and s: "Card_order s"
shows "Card_order (cmax r s)"
unfolding cmax_def by (auto simp: Card_order_csum)
ordLeq_cmax:
assumes r: "Card_order r" and s: "Card_order s"
shows "r ≤o cmax r s ∧ s ≤o cmax r s"
by (meson card_order_on_def cmax1 cmax2 ordIso_iff_ordLeq ordLeq_total ordLeq_transitive r s)
ordLeq_cmax1 = ordLeq_cmax[THEN conjunct1] and
ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2]
finite_cmax:
assumes r: "Card_order r" and s: "Card_order s"
shows "finite (Field (cmax r s)) ⟷ finite (Field r) ∧ finite (Field s)"
by (meson card_order_on_def cmax1 cmax2 ordIso_finite_Field ordLeq_finite_Field ordLeq_total r s)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet am 2026-08-25)
¤
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 und die Messung sind noch experimentell.
