Canonical way of saying "exists a bijection"

Stream: new members

[Wojciech Nawrocki]

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]

You could say that the cardinalities are the same.

[Adam Topaz]

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

[Wojciech Nawrocki]

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

[Junyan Xu]

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]

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

[Junyan Xu]

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

[Yaël Dillies]

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.