First uncountable ordinal

Stream: new members

[Malte Voos]

Hi folks,
I'm participating in a student seminar at my university about formalizing mathematics in Lean, for which I have to formalize a piece of mathematics and present about it in class. I was thinking that formalizing a counterexample from topology could be quite fun; one of my favorites is the "long ray" (https://en.wikipedia.org/wiki/Long_line_(topology)). However I'm already stuck at the very first step because I can't seem to figure out how to construct the first uncountable ordinal in Lean. I've skimmed the files about ordinal numbers in mathlib but couldn't find any useful information. Any hints would be much appreciated! :)

[Malte Voos]

Ohh, it's in SetTheory/Cardinal/Aleph.lean. I'll read that first.

[Aaron Liu]

It's Cardinal.aleph 1

[Kevin Buzzard]

That doesn't sound like an ordinal...

[Kevin Buzzard]

docs#Cardinal.aleph

[Malte Voos]

I found it, omega_1 is defined directly here: https://github.com/leanprover-community/mathlib4/blob/7b4a09d2102c2eae2457af54dfcb57a51e99c5e0/Mathlib/SetTheory/Cardinal/Aleph.lean#L195

[Kevin Buzzard]

It's Ordinal.omega 1

[Kevin Buzzard]

Malte Voos said:

I found it, omega_1 is defined directly here

Even better :-)

[Malte Voos]

Thanks :) Now comes the hard part...