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

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