Ordinals

Stream: new members

[luna elliott]

I'm very new so sorry if I'm being stupid. Each set seems to require its elements to belong to a specific type. This makes me unsure how to translate certain things into lean. For example I don't understand how ordinals work in Lean type theory, it seems that each ordinal (after a point) would require its own type? I also dont know how proof about arbitrary sets would work. For example how would you state that for all infinite sets there is a bijection from that set to its square?

[Aaron Liu]

docs#Ordinal

[Aaron Liu]

docs#Cardinal.mul_eq_self

[Kevin Buzzard]

Lean has universes, which means that there can be one type Ordinal whose terms are ordinals, even though in set theory Ordinal would be a class rather than a set.

[Kevin Buzzard]

A general rule is: in set theory everything is a set, but in type theory there are types (which play the role of sets) and terms (which play the role of elements). Your question about bijecting a set with its square is probably more faithfully translated as

import Mathlib

example
    -- let X be what a set theorist would call a set and what a type theorist would call a type
    (X : Type)
    -- and assume X is infinite
    [Infinite X]
    -- then
    :
    -- there's a bijection between X and X × X
    ∃ f : X → X × X, Function.Bijective f := by
  sorry

rather than the statement about cardinals linked to above, although one could prove it by using the statement about cardinals.

[luna elliott]

Thank you for the explanation!