# Zulip Chat Archive

## Stream: new members

### Topic: Transfinite recursion

#### Lucas Polymeris (Sep 16 2021 at 14:58):

Hi. I'm again having troubles with my set-theoretic view. I've defined a function `f : ordinal → set C`

. I would like

to argue that there must be `α,β ∈ ordinal`

such that `f(α) = f(β)`

. Mathematically I'd do this by actually defining `f`

with

domain `ν`

where `ν`

is any ordinal that does not inject to `℘(C)`

.

Any Idea how this should be done here? I've skimmed through `set_theory.ordinal`

, `set_theory.cardinal`

(and others) and have not had any success.

#### Eric Wieser (Sep 16 2021 at 15:54):

Can you give a #mwe of the statement you want to prove?

#### Lucas Polymeris (Sep 16 2021 at 16:12):

I guess something like this should be close enough:

```
import data.set set_theory.ordinal
open set ordinal
universe u
section
parameters {C : Type u} (g : set C → set C)
def f : ordinal → set C
| ξ := ⋃ η < ξ, g (f η)
using_well_founded { dec_tac := `[assumption] }
lemma some_lemma: ∃ {α β : ordinal}, f α = f β := by sorry
end
```

But keep in mind that so far, defining `f`

from `ordinal`

is the only thing that I've managed to accomplish, If the way to go is to define f some other way, that would be ok too. I'v also tried to define it on the well order of something like `cardinal.ord (cardinal.succ (cardinal.mk (set C))))`

, which should be an ordinal that does not inject to `set C`

, but I did not manage to pull it of.

#### Eric Wieser (Sep 16 2021 at 16:20):

I assume you're missing an `α ≠ β`

component somewhere, else that statement is trivially true

#### Reid Barton (Sep 16 2021 at 16:29):

You probably want to write explicit universe variables like `def f : ordinal.{u} → set C`

, and maybe use `set_option pp.universes true`

to check that your universe levels are what you expect.

#### Eric Wieser (Sep 16 2021 at 16:29):

I'm very surprised this doesn't work:

```
lemma some_lemma: ∃ {α β : ordinal}, f α = f β := ⟨0, 0, begin
refl,
end⟩
```

#### Eric Wieser (Sep 16 2021 at 16:31):

Ah, @Reid Barton's comment reveals the issue with that attempt; your statement is actually `∃ {α : ordinal.{u}} {b : ordinal.{v}}`

#### Reid Barton (Sep 16 2021 at 16:58):

This is ugly (I wrote it in the online Lean editor), but it works:

```
import data.set set_theory.ordinal
open set ordinal
universe u
section
lemma {v} up_injective {X : Type u} :
function.injective (ulift.up.{v} : X → ulift X) :=
begin
rintros x1 x2 h, cc,
end
lemma some_lemma (X : Type u) (f : ordinal.{u} → X) :
¬ function.injective f := begin
let g : ordinal.{u} → ulift.{u+1} X := λ o, ulift.up (f o),
suffices : ¬ function.injective g,
{ intro hf, exact this (up_injective.comp hf) },
intro hg,
replace hg := cardinal.mk_le_of_injective hg,
rw ← cardinal.lift_mk at hg,
replace hg := lt_of_le_of_lt hg (cardinal.lift_lt_univ _),
contrapose! hg,
rw cardinal.univ_id
end
end
```

#### Reid Barton (Sep 16 2021 at 17:03):

Basically `cardinal.lift_lt_univ`

is the key fact, and the rest is shuffling which I probably didn't do very efficiently.

#### Reid Barton (Sep 16 2021 at 17:15):

`up_injective`

already exists as `equiv.ulift.symm.injective`

#### Lucas Polymeris (Sep 16 2021 at 17:17):

Eric Wieser said:

I assume you're missing an

`α ≠ β`

component somewhere, else that statement is trivially true

Yes of course, my bad.

#### Lucas Polymeris (Sep 16 2021 at 17:19):

Reid Barton said:

Basically

`cardinal.lift_lt_univ`

is the key fact, and the rest is shuffling which I probably didn't do very efficiently.

I'll have a look at `cardinal.lift_lt_univ`

. Thanks.

#### Lucas Polymeris (Sep 17 2021 at 14:17):

It worked nicely thanks. Shouldn't something like this or similar be in mathlib? It is quite a common thing to do, I believe.

#### Reid Barton (Sep 17 2021 at 15:50):

I actually meant to ask what you were using this for--a lot of the time you can use an inductive predicate (or impredicative-style definition) for a subset that you might define by transfinite induction in a set-theoretic setting.

#### Reid Barton (Sep 17 2021 at 15:50):

By impredicative-style definition I mean something like "the intersection of all sets `s`

such that `s`

contains `g s`

"

#### Reid Barton (Sep 17 2021 at 15:54):

I guess I should say that I'm more familiar with transfinite constructions in category theory where you're building a sequence of objects so you can't conclude that the sequence stabilizes for size reasons, and have to use some accessibility of `g`

instead (and so you know in advance when to stop).

#### Reid Barton (Sep 17 2021 at 15:56):

But anyways this statement about `¬ function.injective f`

does seem useful for mathlib, and maybe some lemmas that would simplify the proof are missing too.

#### Lucas Polymeris (Sep 17 2021 at 17:35):

@Reid Barton I'm doing something similar to https://core.ac.uk/download/pdf/4886291.pdf (lemma 1). I'm not familiar with category theory, but what you describe sounds similar to what I'm doing.

#### M.G. (Sep 17 2021 at 17:52):

Lucas Polymeris said:

Reid Barton I'm doing something similar to https://core.ac.uk/download/pdf/4886291.pdf (lemma 1). I'm not familiar with category theory, but what you describe sounds similar to what I'm doing.

Awesome, I just started Christopher Allen, Julie Moronuki - Haskell Programming from first principles (2016), I can share my notes if you are interested.

Last updated: Dec 20 2023 at 11:08 UTC