Exact source: Mathlib/SetTheory/Cardinal/Defs.lean
Pinned GitHub source · Raw UTF-8 source
Back to A Naimark counterexample of continuum norm density
1/-2Copyright (c) 2017 Johannes Hölzl. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Johannes Hölzl, Mario Carneiro, Floris van Doorn5-/6module78public import Mathlib.Data.ULift9public import Mathlib.Tactic.CrossRefAttribute10public import Mathlib.Tactic.PPWithUniv11public import Mathlib.Util.Delaborators1213/-!14# Cardinal Numbers1516We define cardinal numbers as a quotient of types under the equivalence relation of equinumerosity17(i.e., existence of a bijection).1819## Main definitions2021* `Cardinal` is the type of cardinal numbers (in a given universe).22* `Cardinal.mk α` or `#α` is the cardinality of `α`. The notation `#` lives in the locale23 `Cardinal`.24* Addition `c₁ + c₂` is defined by `Cardinal.add_def α β : #α + #β = #(α ⊕ β)`.25* Multiplication `c₁ * c₂` is defined by `Cardinal.mul_def : #α * #β = #(α × β)`.26* Exponentiation `c₁ ^ c₂` is defined by `Cardinal.power_def α β : #α ^ #β = #(β → α)`.27* `Cardinal.sum` is the sum of an indexed family of cardinals, i.e. the cardinality of the28 corresponding sigma type.29* `Cardinal.prod` is the product of an indexed family of cardinals, i.e. the cardinality of the30 corresponding pi type.31* `Cardinal.aleph0` or `ℵ₀` is the cardinality of `ℕ`. This definition is universe polymorphic:32 `Cardinal.aleph0.{u} : Cardinal.{u}` (contrast with `ℕ : Type`, which lives in a specific33 universe). In some cases the universe level has to be given explicitly.3435## Implementation notes3637* There is a type of cardinal numbers in every universe level:38 `Cardinal.{u} : Type (u + 1)` is the quotient of types in `Type u`.39 The operation `Cardinal.lift` lifts cardinal numbers to a higher level.40* Cardinal arithmetic specifically for infinite cardinals (like `κ * κ = κ`) is in the file41 `Mathlib/SetTheory/Cardinal/Ordinal.lean`.4243## References4445* <https://en.wikipedia.org/wiki/Cardinal_number>4647## Tags4849cardinal number, cardinal arithmetic, cardinal exponentiation, aleph,50Cantor's theorem, König's theorem, Konig's theorem51-/5253@[expose] public section5455assert_not_exists Monoid5657open List Function Set5859noncomputable section6061universe u v w v' w'6263variable {α β : Type u}6465/-! ### Definition of cardinals -/6667/-- The equivalence relation on types given by equivalence (bijective correspondence) of types.68 Quotienting by this equivalence relation gives the cardinal numbers.69-/70instance Cardinal.isEquivalent : Setoid (Type u) where71 r α β := Nonempty (α ≃ β)72 iseqv := ⟨73 fun α => ⟨Equiv.refl α⟩,74 fun ⟨e⟩ => ⟨e.symm⟩,75 fun ⟨e₁⟩ ⟨e₂⟩ => ⟨e₁.trans e₂⟩⟩7677/-- `Cardinal.{u}` is the type of cardinal numbers in `Type u`,78 defined as the quotient of `Type u` by existence of an equivalence79 (a bijection with explicit inverse). -/80@[pp_with_univ, wikidata Q163875]81def Cardinal : Type (u + 1) :=82 Quotient Cardinal.isEquivalent8384namespace Cardinal8586/-- The cardinal number of a type -/87def mk : Type u → Cardinal :=88 Quotient.mk'8990@[inherit_doc]91scoped prefix:max "#" => Cardinal.mk9293instance canLiftCardinalType : CanLift Cardinal.{u} (Type u) mk fun _ => True :=94 ⟨fun c _ => Quot.inductionOn c fun α => ⟨α, rfl⟩⟩9596@[elab_as_elim]97theorem inductionOn {motive : Cardinal → Prop} (c : Cardinal) (mk : ∀ α, motive #α) : motive c :=98 Quotient.inductionOn c mk99100@[elab_as_elim]101theorem inductionOn₂ {motive : Cardinal → Cardinal → Prop} (c₁ c₂ : Cardinal)102 (mk : ∀ α β, motive #α #β) : motive c₁ c₂ :=103 Quotient.inductionOn₂ c₁ c₂ mk104105@[elab_as_elim]106theorem inductionOn₃ {motive : Cardinal → Cardinal → Cardinal → Prop} (c₁ c₂ c₃ : Cardinal)107 (mk : ∀ α β γ, motive #α #β #γ) : motive c₁ c₂ c₃ :=108 Quotient.inductionOn₃ c₁ c₂ c₃ mk109110theorem induction_on_pi {ι : Type*} {motive : (ι → Cardinal) → Prop}111 (f : ι → Cardinal) (mk : ∀ f : ι → Type v, motive fun i ↦ #(f i)) : motive f :=112 Quotient.induction_on_pi f mk113114protected theorem eq : #α = #β ↔ Nonempty (α ≃ β) :=115 Quotient.eq'116117@[simp]118theorem mk_out (c : Cardinal) : #c.out = c :=119 Quotient.out_eq _120121/-- The representative of the cardinal of a type is equivalent to the original type. -/122def outMkEquiv {α : Type v} : (#α).out ≃ α :=123 Nonempty.some <| Cardinal.eq.mp (by simp)124125theorem mk_congr (e : α ≃ β) : #α = #β :=126 Quot.sound ⟨e⟩127128alias _root_.Equiv.cardinal_eq := mk_congr129130/-- Lift a function between `Type*`s to a function between `Cardinal`s. -/131def map (f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) : Cardinal.{u} → Cardinal.{v} :=132 Quotient.map f fun α β ⟨e⟩ => ⟨hf α β e⟩133134@[simp]135theorem map_mk (f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) (α : Type u) :136 map f hf #α = #(f α) :=137 rfl138139/-- Lift a binary operation `Type* → Type* → Type*` to a binary operation on `Cardinal`s. -/140def map₂ (f : Type u → Type v → Type w) (hf : ∀ α β γ δ, α ≃ β → γ ≃ δ → f α γ ≃ f β δ) :141 Cardinal.{u} → Cardinal.{v} → Cardinal.{w} :=142 Quotient.map₂ f fun α β ⟨e₁⟩ γ δ ⟨e₂⟩ => ⟨hf α β γ δ e₁ e₂⟩143144/-! ### Lifting cardinals to a higher universe -/145146/-- The universe lift operation on cardinals. You can specify the universes explicitly with147 `lift.{u v} : Cardinal.{v} → Cardinal.{max v u}` -/148@[pp_with_univ]149def lift (c : Cardinal.{v}) : Cardinal.{max v u} :=150 map ULift.{u, v} (fun _ _ e => Equiv.ulift.trans <| e.trans Equiv.ulift.symm) c151152@[simp]153theorem mk_uLift (α) : #(ULift.{v, u} α) = lift.{v} #α :=154 rfl155156/-- `lift.{max u v, u}` equals `lift.{v, u}`.157158Unfortunately, the simp lemma doesn't work. -/159theorem lift_umax : lift.{max u v, u} = lift.{v, u} :=160 funext fun a => inductionOn a fun _ => (Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq161162/-- A cardinal lifted to a lower or equal universe equals itself.163164Unfortunately, the simp lemma doesn't work. -/165theorem lift_id' (a : Cardinal.{max u v}) : lift.{u} a = a :=166 inductionOn a fun _ => mk_congr Equiv.ulift167168/-- A cardinal lifted to the same universe equals itself. -/169@[simp]170theorem lift_id (a : Cardinal) : lift.{u, u} a = a :=171 lift_id'.{u, u} a172173/-- A cardinal lifted to the zero universe equals itself. -/174@[simp]175theorem lift_uzero (a : Cardinal.{u}) : lift.{0} a = a :=176 lift_id'.{0, u} a177178@[simp]179theorem lift_lift.{u_1} (a : Cardinal.{u_1}) : lift.{w} (lift.{v} a) = lift.{max v w} a :=180 inductionOn a fun _ => (Equiv.ulift.trans <| Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq181182theorem out_lift_equiv (a : Cardinal.{u}) : Nonempty ((lift.{v} a).out ≃ a.out) := by183 rw [← mk_out a, ← mk_uLift, mk_out]184 exact ⟨outMkEquiv.trans Equiv.ulift⟩185186theorem lift_mk_eq {α : Type u} {β : Type v} :187 lift.{max v w} #α = lift.{max u w} #β ↔ Nonempty (α ≃ β) :=188 Quotient.eq'.trans189 ⟨fun ⟨f⟩ => ⟨Equiv.ulift.symm.trans <| f.trans Equiv.ulift⟩, fun ⟨f⟩ =>190 ⟨Equiv.ulift.trans <| f.trans Equiv.ulift.symm⟩⟩191192/-- A variant of `Cardinal.lift_mk_eq` with specialized universes.193Because Lean often cannot realize it should use this specialization itself,194we provide this statement separately so you don't have to solve the specialization problem either.195-/196theorem lift_mk_eq' {α : Type u} {β : Type v} : lift.{v} #α = lift.{u} #β ↔ Nonempty (α ≃ β) :=197 lift_mk_eq.{u, v, 0}198199theorem mk_congr_lift {α : Type u} {β : Type v} (e : α ≃ β) : lift.{v} #α = lift.{u} #β :=200 lift_mk_eq'.2 ⟨e⟩201202alias _root_.Equiv.lift_cardinal_eq := mk_congr_lift203204/-! ### Basic cardinals -/205206instance : Zero Cardinal.{u} :=207 -- `PEmpty` might be more canonical, but this is convenient for defeq with natCast208 ⟨lift #(Fin 0)⟩209210instance : Inhabited Cardinal.{u} :=211 ⟨0⟩212213@[simp]214theorem mk_eq_zero (α : Type u) [IsEmpty α] : #α = 0 :=215 (Equiv.equivOfIsEmpty α (ULift (Fin 0))).cardinal_eq216217@[simp]218theorem lift_zero : lift 0 = 0 := mk_eq_zero _219220theorem mk_eq_zero_iff {α : Type u} : #α = 0 ↔ IsEmpty α :=221 ⟨fun e =>222 let ⟨h⟩ := Quotient.exact e223 h.isEmpty,224 @mk_eq_zero α⟩225226theorem mk_ne_zero_iff {α : Type u} : #α ≠ 0 ↔ Nonempty α :=227 (not_iff_not.2 mk_eq_zero_iff).trans not_isEmpty_iff228229@[simp]230theorem mk_ne_zero (α : Type u) [Nonempty α] : #α ≠ 0 :=231 mk_ne_zero_iff.2 ‹_›232233theorem nonempty_out {x : Cardinal} (h : x ≠ 0) : Nonempty x.out := by234 rwa [← mk_ne_zero_iff, mk_out]235236instance : One Cardinal.{u} :=237 -- `PUnit` might be more canonical, but this is convenient for defeq with natCast238 ⟨lift #(Fin 1)⟩239240instance : Nontrivial Cardinal.{u} :=241 ⟨⟨1, 0, mk_ne_zero _⟩⟩242243theorem mk_eq_one (α : Type u) [Subsingleton α] [Nonempty α] : #α = 1 :=244 let ⟨_⟩ := nonempty_unique α; (Equiv.ofUnique α (ULift (Fin 1))).cardinal_eq245246instance : Add Cardinal.{u} :=247 ⟨map₂ Sum fun _ _ _ _ => Equiv.sumCongr⟩248249theorem add_def (α β : Type u) : #α + #β = #(α ⊕ β) :=250 rfl251252instance : NatCast Cardinal.{u} :=253 ⟨fun n => lift #(Fin n)⟩254255@[simp]256theorem mk_sum (α : Type u) (β : Type v) : #(α ⊕ β) = lift.{v, u} #α + lift.{u, v} #β :=257 mk_congr (Equiv.ulift.symm.sumCongr Equiv.ulift.symm)258259@[simp]260theorem mk_option {α : Type u} : #(Option α) = #α + 1 := by261 rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]262263@[simp]264theorem mk_psum (α : Type u) (β : Type v) : #(α ⊕' β) = lift.{v} #α + lift.{u} #β :=265 (mk_congr (Equiv.psumEquivSum α β)).trans (mk_sum α β)266267instance : Mul Cardinal.{u} :=268 ⟨map₂ Prod fun _ _ _ _ => Equiv.prodCongr⟩269270theorem mul_def (α β : Type u) : #α * #β = #(α × β) :=271 rfl272273@[simp]274theorem mk_prod (α : Type u) (β : Type v) : #(α × β) = lift.{v, u} #α * lift.{u, v} #β :=275 mk_congr (Equiv.ulift.symm.prodCongr Equiv.ulift.symm)276277/-- The cardinal exponential. `#α ^ #β` is the cardinal of `β → α`. -/278instance instPowCardinal : Pow Cardinal.{u} Cardinal.{u} :=279 ⟨map₂ (fun α β => β → α) fun _ _ _ _ e₁ e₂ => e₂.arrowCongr e₁⟩280281theorem power_def (α β : Type u) : #α ^ #β = #(β → α) :=282 rfl283284theorem mk_arrow (α : Type u) (β : Type v) : #(α → β) = (lift.{u} #β ^ lift.{v} #α) :=285 mk_congr (Equiv.ulift.symm.arrowCongr Equiv.ulift.symm)286287@[simp]288theorem lift_power (a b : Cardinal.{u}) : lift.{v} (a ^ b) = lift.{v} a ^ lift.{v} b :=289 inductionOn₂ a b fun _ _ =>290 mk_congr <| Equiv.ulift.trans (Equiv.ulift.arrowCongr Equiv.ulift).symm291292@[simp]293theorem power_zero (a : Cardinal) : a ^ (0 : Cardinal) = 1 :=294 inductionOn a fun _ => mk_eq_one _295296@[simp]297theorem power_one (a : Cardinal.{u}) : a ^ (1 : Cardinal) = a :=298 inductionOn a fun α => mk_congr (Equiv.funUnique (ULift.{u} (Fin 1)) α)299300theorem power_add (a b c : Cardinal) : a ^ (b + c) = a ^ b * a ^ c :=301 inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumArrowEquivProdArrow β γ α302303@[simp]304theorem one_power {a : Cardinal} : (1 : Cardinal) ^ a = 1 :=305 inductionOn a fun _ => mk_eq_one _306307@[simp]308theorem zero_power {a : Cardinal} : a ≠ 0 → (0 : Cardinal) ^ a = 0 :=309 inductionOn a fun _ heq =>310 mk_eq_zero_iff.2 <|311 isEmpty_pi.2 <|312 let ⟨a⟩ := mk_ne_zero_iff.1 heq313 ⟨a, inferInstance⟩314315theorem power_ne_zero {a : Cardinal} (b : Cardinal) : a ≠ 0 → a ^ b ≠ 0 :=316 inductionOn₂ a b fun _ _ h =>317 let ⟨a⟩ := mk_ne_zero_iff.1 h318 mk_ne_zero_iff.2 ⟨fun _ => a⟩319320theorem mul_power {a b c : Cardinal} : (a * b) ^ c = a ^ c * b ^ c :=321 inductionOn₃ a b c fun _ _ γ => mk_congr <| Equiv.arrowProdEquivProdArrow γ _ _322323@[simp]324theorem lift_one : lift 1 = 1 := mk_eq_one _325326@[simp]327theorem lift_add (a b : Cardinal.{u}) : lift.{v} (a + b) = lift.{v} a + lift.{v} b :=328 inductionOn₂ a b fun _ _ =>329 mk_congr <| Equiv.ulift.trans (Equiv.sumCongr Equiv.ulift Equiv.ulift).symm330331/-! ### Indexed cardinal `sum` -/332333/-- The indexed sum of cardinals is the cardinality of the334 indexed disjoint union, i.e. sigma type. -/335def sum {ι} (f : ι → Cardinal) : Cardinal :=336 mk (Σ i, (f i).out)337338@[simp]339theorem mk_sigma {ι} (f : ι → Type*) : #(Σ i, f i) = sum fun i => #(f i) :=340 mk_congr <| Equiv.sigmaCongrRight fun _ => outMkEquiv.symm341342theorem mk_sigma_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'}343 (e : ι ≃ ι') (h : ∀ i, lift.{w'} #(f i) = lift.{w} #(g (e i))) :344 lift.{max v' w'} #(Σ i, f i) = lift.{max v w} #(Σ i, g i) :=345 Cardinal.lift_mk_eq'.2 ⟨.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.lift_mk_eq'.1 (h i)⟩346347theorem mk_sigma_congr {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι')348 (h : ∀ i, #(f i) = #(g (e i))) : #(Σ i, f i) = #(Σ i, g i) :=349 mk_congr <| Equiv.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)350351/-- Similar to `mk_sigma_congr` with indexing types in different universes. This is not a strict352generalization. -/353theorem mk_sigma_congr' {ι : Type u} {ι' : Type v} {f : ι → Type max w (max u v)}354 {g : ι' → Type max w (max u v)} (e : ι ≃ ι')355 (h : ∀ i, #(f i) = #(g (e i))) : #(Σ i, f i) = #(Σ i, g i) :=356 mk_congr <| Equiv.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)357358theorem mk_sigma_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :359 #(Σ i, f i) = #(Σ i, g i) :=360 mk_sigma_congr (Equiv.refl ι) h361362theorem mk_psigma_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :363 #(Σ' i, f i) = #(Σ' i, g i) :=364 mk_congr <| .psigmaCongrRight fun i => Classical.choice <| Cardinal.eq.mp (h i)365366theorem mk_psigma_congrRight_prop {ι : Prop} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :367 #(Σ' i, f i) = #(Σ' i, g i) :=368 mk_congr <| .psigmaCongrRight fun i => Classical.choice <| Cardinal.eq.mp (h i)369370theorem mk_sigma_arrow {ι} (α : Type*) (f : ι → Type*) :371 #(Sigma f → α) = #(Π i, f i → α) := mk_congr <| Equiv.piCurry fun _ _ ↦ α372373@[simp]374theorem sum_const (ι : Type u) (a : Cardinal.{v}) :375 (sum fun _ : ι => a) = lift.{v} #ι * lift.{u} a :=376 inductionOn a fun α =>377 mk_congr <|378 calc379 (Σ _ : ι, Quotient.out #α) ≃ ι × Quotient.out #α := Equiv.sigmaEquivProd _ _380 _ ≃ ULift ι × ULift α := Equiv.ulift.symm.prodCongr (outMkEquiv.trans Equiv.ulift.symm)381382theorem sum_const' (ι : Type u) (a : Cardinal.{u}) : (sum fun _ : ι => a) = #ι * a := by simp383384@[simp]385theorem lift_sum {ι : Type u} (f : ι → Cardinal.{v}) :386 Cardinal.lift.{w} (Cardinal.sum f) = Cardinal.sum fun i => Cardinal.lift.{w} (f i) :=387 Equiv.cardinal_eq <|388 Equiv.ulift.trans <|389 Equiv.sigmaCongrRight fun a =>390 -- Porting note: Inserted universe hint .{_,_,v} below391 Nonempty.some <| by rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]392393theorem sum_nat_eq_add_sum_succ (f : ℕ → Cardinal.{u}) :394 Cardinal.sum f = f 0 + Cardinal.sum fun i => f (i + 1) := by395 refine (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_396 simp only [mk_sum, mk_out, lift_id, mk_sigma]397398/-! ### Indexed cardinal `prod` -/399400/-- The indexed product of cardinals is the cardinality of the Pi type401 (dependent product). -/402def prod {ι : Type u} (f : ι → Cardinal) : Cardinal :=403 #(Π i, (f i).out)404405@[simp]406theorem mk_pi {ι : Type u} (α : ι → Type v) : #(Π i, α i) = prod fun i => #(α i) :=407 mk_congr <| Equiv.piCongrRight fun _ => outMkEquiv.symm408409theorem mk_pi_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'}410 (e : ι ≃ ι') (h : ∀ i, lift.{w'} #(f i) = lift.{w} #(g (e i))) :411 lift.{max v' w'} #(Π i, f i) = lift.{max v w} #(Π i, g i) :=412 Cardinal.lift_mk_eq'.2 ⟨.piCongr e fun i ↦ Classical.choice <| Cardinal.lift_mk_eq'.1 (h i)⟩413414theorem mk_pi_congr {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι')415 (h : ∀ i, #(f i) = #(g (e i))) : #(Π i, f i) = #(Π i, g i) :=416 mk_congr <| Equiv.piCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)417418theorem mk_pi_congr_prop {ι ι' : Prop} {f : ι → Type v} {g : ι' → Type v} (e : ι ↔ ι')419 (h : ∀ i, #(f i) = #(g (e.mp i))) : #(Π i, f i) = #(Π i, g i) :=420 mk_congr <| Equiv.piCongr (.ofIff e) fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)421422/-- Similar to `mk_pi_congr` with indexing types in different universes. This is not a strict423generalization. -/424theorem mk_pi_congr' {ι : Type u} {ι' : Type v} {f : ι → Type max w (max u v)}425 {g : ι' → Type max w (max u v)} (e : ι ≃ ι')426 (h : ∀ i, #(f i) = #(g (e i))) : #(Π i, f i) = #(Π i, g i) :=427 mk_congr <| Equiv.piCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)428429theorem mk_pi_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :430 #(Π i, f i) = #(Π i, g i) :=431 mk_pi_congr (Equiv.refl ι) h432433theorem mk_pi_congrRight_prop {ι : Prop} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :434 #(Π i, f i) = #(Π i, g i) :=435 mk_pi_congr_prop Iff.rfl h436437@[simp]438theorem prod_const (ι : Type u) (a : Cardinal.{v}) :439 (prod fun _ : ι => a) = lift.{u} a ^ lift.{v} #ι :=440 inductionOn a fun _ =>441 mk_congr <| Equiv.piCongr Equiv.ulift.symm fun _ => outMkEquiv.trans Equiv.ulift.symm442443theorem prod_const' (ι : Type u) (a : Cardinal.{u}) : (prod fun _ : ι => a) = a ^ #ι :=444 inductionOn a fun _ => (mk_pi _).symm445446@[simp]447theorem prod_eq_zero {ι} (f : ι → Cardinal.{u}) : prod f = 0 ↔ ∃ i, f i = 0 := by448 lift f to ι → Type u using fun _ => trivial449 simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]450451theorem prod_ne_zero {ι} (f : ι → Cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0 := by simp [prod_eq_zero]452453theorem lift_power_sum {ι : Type u} (a : Cardinal.{v}) (f : ι → Cardinal.{v}) :454 lift.{u, v} a ^ sum f = prod fun i ↦ a ^ f i := by455 induction a using Cardinal.inductionOn with | _ α =>456 induction f using induction_on_pi with | _ f =>457 simp_rw [← mk_uLift, prod, sum, power_def]458 apply mk_congr459 refine (Equiv.piCurry fun _ _ => ULift α).trans ?_460 refine Equiv.piCongrRight fun b => ?_461 refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_462 exact outMkEquiv.symm463464theorem power_sum {ι : Type u} (a : Cardinal.{max u v}) (f : ι → Cardinal.{max u v}) :465 a ^ sum f = prod fun i ↦ a ^ f i := by466 simpa [← lift_umax] using lift_power_sum a f467468@[simp]469theorem lift_prod {ι : Type u} (c : ι → Cardinal.{v}) :470 lift.{w} (prod c) = prod fun i => lift.{w} (c i) := by471 lift c to ι → Type v using fun _ => trivial472 simp only [← mk_pi, ← mk_uLift]473 exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)474475/-! ### The first infinite cardinal `aleph0` -/476477/-- `ℵ₀` is the smallest infinite cardinal. -/478def aleph0 : Cardinal.{u} :=479 lift #ℕ480481@[inherit_doc] scoped notation "ℵ₀" => Cardinal.aleph0482recommended_spelling "aleph0" for "ℵ₀" in [aleph0, «termℵ₀»]483484theorem mk_nat : #ℕ = ℵ₀ :=485 (lift_id _).symm486487theorem aleph0_ne_zero : ℵ₀ ≠ 0 :=488 mk_ne_zero _489490@[simp]491theorem lift_aleph0 : lift ℵ₀ = ℵ₀ :=492 lift_lift _493494theorem lift_mk_fin (n : ℕ) : lift #(Fin n) = n := rfl495496/-! ### Cardinalities of basic sets and types -/497498theorem mk_empty : #Empty = 0 :=499 mk_eq_zero _500501theorem mk_pempty : #PEmpty = 0 :=502 mk_eq_zero _503504theorem mk_punit : #PUnit = 1 :=505 mk_eq_one PUnit506507theorem mk_unit : #Unit = 1 :=508 mk_punit509510theorem mk_plift_true : #(PLift True) = 1 :=511 mk_eq_one _512513theorem mk_plift_false : #(PLift False) = 0 :=514 mk_eq_zero _515516theorem mk_subtype_of_equiv {α β : Type u} (p : β → Prop) (e : α ≃ β) :517 #{ a : α // p (e a) } = #{ b : β // p b } :=518 mk_congr (Equiv.subtypeEquivOfSubtype e)519520end Cardinal521522-- namespace Tactic523524-- open Cardinal Positivity525526-- Porting note: Meta code, do not port directly527-- /-- Extension for the `positivity` tactic: The cardinal power of a positive cardinal is528-- positive. -/529-- @[positivity]530-- unsafe def positivity_cardinal_pow : expr → tactic strictness531-- | q(@Pow.pow _ _ $(inst) $(a) $(b)) => do532-- let strictness_a ← core a533-- match strictness_a with534-- | positive p => positive <$> mk_app `` power_pos [b, p]535-- | _ => failed536-- |-- We already know that `0 ≤ x` for all `x : Cardinal`537-- _ =>538-- failed539540-- end Tactic