# Zulip Chat Archive

## 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 `S`

s as `timed_S`

s

#### 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):

#### 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):

coincidentally, https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib.3Amaster/near/264693273

Last updated: Dec 20 2023 at 11:08 UTC