theory Konig imports Cofinality Cardinal_Library begin text‹Now, using the Axiom of choice, we can show that all successor cardinals are regular.› lemma cf_csucc: assumes "InfCard(z)" shows "cf(z⇧^{+}) = z⇧^{+}" proof (rule ccontr) assume "cf(z⇧^{+}) ≠ z⇧^{+}" moreover from ‹InfCard(z)› have "Ord(z⇧^{+})" "Ord(z)" "Limit(z)" "Limit(z⇧^{+})" "Card(z⇧^{+})" "Card(z)" using InfCard_csucc Card_is_Ord InfCard_is_Card InfCard_is_Limit by fastforce+ moreover from calculation have "cf(z⇧^{+}) < z⇧^{+}" using cf_le_cardinal[of "z⇧^{+}", THEN le_iff[THEN iffD1]] Card_cardinal_eq by simp ultimately obtain G where "G:cf(z⇧^{+})→ z⇧^{+}" "∀β∈z⇧^{+}. ∃y∈cf(z⇧^{+}). β < G`y" using Limit_cofinal_fun_lt[of "z⇧^{+}" _ "cf(z⇧^{+})"] Ord_cf cf_le_cf_fun[of "z⇧^{+}" "cf(z⇧^{+})"] le_refl[of "cf(z⇧^{+})"] by auto with ‹Card(z)› ‹Card(z⇧^{+})› ‹Ord(z⇧^{+})› have "∀β∈cf(z⇧^{+}). |G`β| ≤ z" using apply_type[of G "cf(z⇧^{+})" "λ_. z⇧^{+}", THEN ltI] Card_lt_iff[THEN iffD2] Ord_in_Ord[OF Card_is_Ord, of "z⇧^{+}"] cardinal_lt_csucc_iff[THEN iffD1] by auto from ‹cf(z⇧^{+}) < z⇧^{+}› ‹InfCard(z)› ‹Ord(z)› have "cf(z⇧^{+}) ≲ z" using cardinal_lt_csucc_iff[of "z" "cf(z⇧^{+})"] Card_csucc[of "z"] le_Card_iff[of "z" "cf(z⇧^{+})"] InfCard_is_Card Card_lt_iff[of "cf(z⇧^{+})" "z⇧^{+}"] lt_Ord[of "cf(z⇧^{+})" "z⇧^{+}"] by simp with ‹cf(z⇧^{+}) < z⇧^{+}› ‹∀β∈cf(z⇧^{+}). |G`β| ≤ _› ‹InfCard(z)› have "|⋃β∈cf(z⇧^{+}). G`β| ≤ z" using InfCard_csucc[of z] subset_imp_lepoll[THEN lepoll_imp_cardinal_le, of "⋃β∈cf(z⇧^{+}). G`β" "z"] by (rule_tac lepoll_imp_cardinal_UN_le) auto moreover note ‹Ord(z)› moreover from ‹∀β∈z⇧^{+}. ∃y∈cf(z⇧^{+}). β < G`y› and this have "z⇧^{+}⊆ (⋃β∈cf(z⇧^{+}). G`β)" by (blast dest:ltD) ultimately have "z⇧^{+}≤ z" using subset_imp_le_cardinal[of "z⇧^{+}" "⋃β∈cf(z⇧^{+}). G`β"] le_trans InfCard_is_Card Card_csucc[of z] Card_cardinal_eq by auto with ‹Ord(z)› show "False" using lt_csucc[of z] not_lt_iff_le[THEN iffD2, of z "z⇧^{+}"] Card_csucc[THEN Card_is_Ord] by auto qed text‹And this finishes the calculation of cofinality of Alephs.› lemma cf_Aleph_succ: "Ord(z) ⟹ cf(ℵ⇘succ(z)⇙) = ℵ⇘succ(z)⇙" using Aleph_succ cf_csucc InfCard_Aleph by simp subsection‹König's Theorem\label{sec:konig}› text‹We end this section by proving König's Theorem on the cofinality of cardinal exponentiation. This is a strengthening of Cantor's theorem and it is essentially the only basic way to prove strict cardinal inequalities. It is proved rather straightforwardly with the tools already developed.› lemma konigs_theorem: notes [dest] = InfCard_is_Card Card_is_Ord and [trans] = lt_trans1 lt_trans2 assumes "InfCard(κ)" "InfCard(ν)" "cf(κ) ≤ ν" shows "κ < κ⇗↑ν⇖" using assms(1,2) Card_cexp proof (intro not_le_iff_lt[THEN iffD1] notI) assume "κ⇗↑ν⇖ ≤ κ" moreover note ‹InfCard(κ)› moreover from calculation have "ν → κ ≲ κ" using Card_cardinal_eq[OF InfCard_is_Card, symmetric] Card_le_imp_lepoll unfolding cexp_def by simp ultimately obtain G where "G ∈ surj(κ, ν → κ)" using inj_imp_surj[OF _ function_space_nonempty, OF _ nat_into_InfCard] by blast from assms obtain f where "f:ν → κ" "cf_fun(f,κ)" using cf_le_cf_fun[OF _ InfCard_is_Limit] by blast define H where "H(α) ≡ μ x. x∈κ ∧ (∀m<f`α. G`m`α ≠ x)" (is "_ ≡ μ x. ?P(α,x)") for α have H_satisfies: "?P(α,H(α))" if "α ∈ ν" for α proof - obtain h where "?P(α,h)" proof - from ‹α∈ν› ‹f:ν → κ› ‹InfCard(κ)› have "f`α < κ" using apply_type[of _ _ "λ_ . κ"] by (auto intro:ltI) have "|{G`m`α . m ∈ {x∈κ . x < f`α}}| ≤ |{x∈κ . x < f`α}|" using cardinal_RepFun_le by simp also from ‹f`α < κ› ‹InfCard(κ)› have "|{x∈κ . x < f`α}| < |κ|" using Card_lt_iff[OF lt_Ord, THEN iffD2, of "f`α" κ κ] Ord_eq_Collect_lt[of "f`α" κ] Card_cardinal_eq by force finally have "|{G`m`α . m ∈ {x∈κ . x < f`α}}| < |κ|" . moreover from ‹f`α < κ› ‹InfCard(κ)› have "m<f`α ⟹ m∈κ" for m using Ord_trans[of m "f`α" κ] by (auto dest:ltD) ultimately have "∃h. ?P(α,h)" using lt_cardinal_imp_not_subset by blast with that show ?thesis by blast qed with assms show "?P(α,H(α))" using LeastI[of "?P(α)" h] lt_Ord Ord_in_Ord unfolding H_def by fastforce qed then have "(λα∈ν. H(α)): ν → κ" using lam_type by auto with ‹G ∈ surj(κ, ν → κ)› obtain n where "n∈κ" "G`n = (λα∈ν. H(α))" unfolding surj_def by blast moreover note ‹InfCard(κ)› ‹f: ν → κ› ‹cf_fun(f,_)› ultimately obtain α where "n < f`α" "α∈ν" using Limit_cofinal_fun_lt[OF InfCard_is_Limit] by blast moreover from calculation and ‹G`n = (λα∈ν. H(α))› have "G`n`α = H(α)" using ltD by simp moreover from calculation and H_satisfies have "∀m<f`α. G`m`α ≠ H(α)" by simp ultimately show "False" by blast qed blast+ lemma cf_cexp: assumes "Card(κ)" "InfCard(ν)" "2 ≤ κ" shows "ν < cf(κ⇗↑ν⇖)" proof (rule ccontr) assume "¬ ν < cf(κ⇗↑ν⇖)" with ‹InfCard(ν)› have "cf(κ⇗↑ν⇖) ≤ ν" using not_lt_iff_le Ord_cf InfCard_is_Card Card_is_Ord by simp moreover note assms moreover from calculation have "InfCard(κ⇗↑ν⇖)" using InfCard_cexp by simp moreover from calculation have "κ⇗↑ν⇖ < (κ⇗↑ν⇖)⇗↑ν⇖" using konigs_theorem by simp ultimately show "False" using cexp_cexp_cmult InfCard_csquare_eq by auto qed text‹Finally, the next two corollaries illustrate the only possible exceptions to the value of the cardinality of the continuum: The limit cardinals of countable cofinality. That these are the only exceptions is a consequence of Easton's Theorem~\<^cite>‹‹Thm 15.18› in "Jech_Millennium"›.› corollary cf_continuum: "ℵ⇘0⇙ < cf(2⇗↑ℵ⇘0⇙⇖)" using cf_cexp InfCard_Aleph nat_into_Card by simp corollary continuum_not_eq_Aleph_nat: "2⇗↑ℵ⇘0⇙⇖ ≠ ℵ⇘ω⇙" using cf_continuum cf_Aleph_Limit[OF Limit_nat] cf_nat Aleph_zero_eq_nat by auto end