## Stream: new members

### Topic: Canonical way of saying "exists a bijection"

#### Wojciech Nawrocki (Jan 12 2023 at 02:25):

What is the mathlib-approved way of stating that two sets X Y : set α are in bijection, as a proposition? My first thought was to use equiv like X ≃ Y, but this lives in Type wheras I just want a Prop. There are a few possible ways of saying what I want, e.g. ∃ f, bijective f or nonempty (X ≃ Y) but it seems like there should be a notation or name for it which we'd already know to be symmetric, transitive etc.

#### Adam Topaz (Jan 12 2023 at 03:14):

You could say that the cardinalities are the same.

#### Adam Topaz (Jan 12 2023 at 03:15):

I don't think we have a definition of the form exists_bijection or in_bijection_with

#### Wojciech Nawrocki (Jan 12 2023 at 03:25):

I see, maybe this is not a common use case. Thanks!

#### Junyan Xu (Jan 12 2023 at 03:32):

The cardinal approach has the inconvenience that if X and Y are in different universes then you have to docs#cardinal.lift the cardinals to the same universe to equate them.

#### Johan Commelin (Jan 12 2023 at 05:10):

I think I would go for nonempty (X ≃ Y)

#### Junyan Xu (Jan 12 2023 at 05:13):

I think so; for transitivity you can use docs#nonempty.map2 with docs#equiv.trans

#### Yaël Dillies (Jan 12 2023 at 08:55):

Junyan Xu said:

The cardinal approach has the inconvenience that if X and Y are in different universes then you have to docs#cardinal.lift the cardinals to the same universe to equate them.

Wojciech explicitly said they had the same type, though.

Last updated: Dec 20 2023 at 11:08 UTC