## Stream: general

### Topic: inductive sets and cardinality

#### Violeta Hernández (Dec 11 2021 at 16:06):

I have an inductive set that’s roughly built up like this

• It includes all ordinals less than Aleph n
• It includes sums of ordinals in the set
• It includes applications of some ordinal function to values in the set

I want to prove that the minimum excluded value of this set is strictly smaller than Aleph (n + 1). The way I’m thinking to do this is by induction on the “height” of an element of the set; at each step I have Aleph n ordinals, and after countably many steps I will still. I’m pretty much lost on what the best way to do this in Lean is, though.

#### Reid Barton (Dec 11 2021 at 16:08):

Does "sums" mean binary/finite sums?

#### Violeta Hernández (Dec 11 2021 at 16:09):

Yep (I used binary sums for simplicity)

#### Reid Barton (Dec 11 2021 at 16:17):

so something like this?

import set_theory.cardinal_ordinal

universe u
variables (n : ℕ) (f : ordinal.{u} → ordinal.{u})

inductive S : ordinal.{u} → Prop
| low : ∀ o, o < (cardinal.aleph n).ord → S o
| add : ∀ o o', S o → S o' → S (o + o')
| app : ∀ o, S o → S (f o)


#### Violeta Hernández (Dec 11 2021 at 16:17):

Yeah, that’s pretty much it

#### Violeta Hernández (Dec 11 2021 at 16:18):

I’m thinking… if I were given some injection from sets of “height” k to Aleph n, I could build an injection from sets of height k + 1 to (Aleph n x Aleph n) + Aleph n, which should then allow me to build an injection from those sets to Aleph n. So overall, I should have an injection from all of these sets to N.card x Aleph n which should then inject into Aleph n as well. Is this the right approach for problems like these?

#### Violeta Hernández (Dec 11 2021 at 16:19):

Not sure if I should phrase things in terms of injections, or just in terms of cardinalities

#### Reid Barton (Dec 11 2021 at 16:32):

So the general strategy that I use for this is to introduce an auxiliary inductive type which indexes the possible "shapes" of the terms of S (which for some reason I call time) and another inductive type which is parameterized by it:

import set_theory.cardinal_ordinal

universe u
variables (n : ℕ) (f : ordinal.{u} → ordinal.{u})

inductive S : ordinal.{u} → Prop
| low : ∀ o, o < (cardinal.aleph n).ord → S o
| add : ∀ o o', S o → S o' → S (o + o')
| app : ∀ o, S o → S (f o)

inductive time
| t_low : time
| t_add : time → time → time
| t_app : time → time
open time

lemma countable_time : cardinal.mk time = cardinal.omega := sorry

inductive timed_S : ordinal.{u} → time → Type (u+1)
| low : ∀ o, o < (cardinal.aleph n).ord → timed_S o t_low
| add : ∀ o t o' t', timed_S o t → timed_S o' t' → timed_S (o + o') (t_add t t')
| app : ∀ o t, timed_S o t → timed_S (f o) (t_app t)

lemma exists_time (o : ordinal.{u}) (h : S n f o) : ∃ t, nonempty (timed_S n f o t) :=
begin
induction h,
{ refine ⟨t_low, ⟨timed_S.low _ _⟩⟩, assumption },
{ sorry },
{ sorry }
end

lemma timed_small (t : time) : cardinal.mk (Σ o, timed_S n f o t) < cardinal.aleph (n+1) :=
begin
induction t with t₁ t₂ h₁ h₂ t' h',
{ sorry },
{ let F :
(Σ (o : ordinal), timed_S n f o t₁) × (Σ (o : ordinal), timed_S n f o t₂) →
(Σ (o : ordinal), timed_S n f o (t_add t₁ t₂)) :=
λ ⟨⟨o, s⟩, ⟨o', s'⟩⟩, ⟨o + o', timed_S.add o t₁ o' t₂ s s'⟩,
have : function.surjective F,
{ rintro ⟨_, s⟩,
cases s with _ _ o t₁ o' t₂ s₁ s₂,
exact ⟨(⟨o, s₁⟩, ⟨o', s₂⟩), rfl⟩ },
refine lt_of_le_of_lt (cardinal.mk_le_of_surjective this) _,
sorry },
{ sorry }
end


#### Reid Barton (Dec 11 2021 at 16:35):

Then, by combining these lemmas, you get a surjection from something whose cardinality you can bound by aleph (n+1) to {o | S n f o}

#### Violeta Hernández (Dec 11 2021 at 16:35):

Wait, small question regarding induction h

#### Violeta Hernández (Dec 11 2021 at 16:35):

Why doesn't cases h work?

#### Reid Barton (Dec 11 2021 at 16:36):

In the other cases, you will need the induction hypothesis to know that you can build the constituent Ss as timed_Ss

#### Reid Barton (Dec 11 2021 at 16:37):

It might end up being that proving countable_time is the most annoying part, in which case I didn't improve much on what you were already suggesting...

#### Reid Barton (Dec 11 2021 at 16:43):

So I guess a variant that combines both is to replace time by nat and timed_S by

inductive timed_S' : ordinal.{u} → ℕ → Type (u+1)
| low : ∀ o, o < (cardinal.aleph n).ord → timed_S' o 0
| add : ∀ o t o' t' t'', timed_S' o t → timed_S' o' t' → t < t'' → t' < t'' → timed_S' (o + o') t''
| app : ∀ o t t', timed_S' o t → t < t' → timed_S' (f o) t'


(there's no real need to generate each element exactly once) and use strong induction to prove timed_small, with more complicated F & cardinal arithmetic there

#### Violeta Hernández (Dec 11 2021 at 17:07):

This is a bit off-topic, but are there any statements about additive principal ordinals? I'm stuck proving a statement of the form a < (cardinal.aleph n).ord → b < (cardinal.aleph n).ord → a + b < (cardinal.aleph n).ord.

#### Violeta Hernández (Dec 11 2021 at 17:16):

The lemmas α < omega ^ γ → β < omega ^ γ → α + β < omega ^ γ and (cardinal.aleph n).ord = omega ^ (cardinal.aleph n).ord  would suffice for this, but I don't think either of them exist...

#### Violeta Hernández (Dec 11 2021 at 17:20):

The first of these lemmas should be provable by building the Cantor Normal Form of α and β. Not sure how I'd tackle the second.

#### Violeta Hernández (Dec 11 2021 at 17:20):

Ah, found ordinal.add_lt_omega_power

#### Violeta Hernández (Dec 11 2021 at 17:33):

I have no idea how to prove the second part though :pensive:

#### Violeta Hernández (Dec 11 2021 at 17:35):

I believe the lemma α < ℵ_n → ω ^ α < ℵ_n should do it, after that I could just use the definition of ordinal exponentiation

#### Violeta Hernández (Dec 11 2021 at 17:39):

(in fact, this lemma should generalize to α < ℵ_n → β < ℵ_n → α ^ β < ℵ_n, which would then allow one to prove α < ℵ_n → α ^ ℵ_n = ℵ_n)

#### Violeta Hernández (Dec 11 2021 at 18:46):

...I have yet another question pertaining to ordinals. Can I prove (cardinal.aleph.{u} n).lift = cardinal.aleph.{u+1} n for n : ℕ?

#### Violeta Hernández (Dec 11 2021 at 18:47):

(or more generally, cardinal.aleph (α.lift) = (cardinal.aleph α).lift)

#### Kevin Buzzard (Dec 11 2021 at 18:54):

Is it definitely true? I'm serious.

#### Kevin Buzzard (Dec 11 2021 at 18:55):

I somehow imagine that changing your universe of sets can screw up cardinals. But I might be way off.

#### Kevin Buzzard (Dec 11 2021 at 18:56):

I'm not even sure if I believe an inequality. But I might just be being paranoid.

#### Violeta Hernández (Dec 11 2021 at 19:12):

I have no idea, but if it isn't true, there goes the last hour of my life :sob:

#### Violeta Hernández (Dec 11 2021 at 19:12):

There's a lot of lift lemmas for ordinals, so I'm at least hopeful

#### Violeta Hernández (Dec 11 2021 at 19:13):

In the best case scenario, this would be true:

theorem cardinal.aleph_lift (α : ordinal.{u}) :
cardinal.aleph (ordinal.lift.{max v u} α) = cardinal.lift.{max v u} (cardinal.aleph.{u} α) :=
sorry


#### Mario Carneiro (Dec 12 2021 at 22:43):

that theorem should be true

#### Mario Carneiro (Dec 12 2021 at 22:44):

Actually you can generalize it to

theorem cardinal.aleph_lift (α : ordinal.{u}) :
cardinal.aleph (ordinal.lift.{v} α) = cardinal.lift.{v} (cardinal.aleph.{u} α) :=
sorry


#### Mario Carneiro (Dec 12 2021 at 22:46):

The stuff about α < ℵ_n → ω ^ α < ℵ_n should generalize to a class of ordinals, I think they are called additive indecomposable ordinals

#### Reid Barton (Dec 13 2021 at 04:04):

Violeta Hernández said:

This is a bit off-topic, but are there any statements about additive principal ordinals? I'm stuck proving a statement of the form a < (cardinal.aleph n).ord → b < (cardinal.aleph n).ord → a + b < (cardinal.aleph n).ord.

Isn't a < x.ord equivalent to a.card < x? (Since x.ord is the smallest ordinal with cardinal x.)
Then it transposes to a more basic fact about the sum of infinite cardinals right?

#### Reid Barton (Dec 13 2021 at 04:05):

docs#cardinal.lt_ord

#### Kevin Buzzard (Dec 13 2021 at 09:28):

ord and card form a Galois insertion or coinsertion I guess.

#### Kevin Buzzard (Dec 13 2021 at 12:34):

Last updated: Aug 03 2023 at 10:10 UTC