equivalence between bounded integers and nat

Stream: maths

[Filippo A. E. Nuccio]

I am wondering if mathlib has the equivalence (N : ℤ) : ℕ ≃ {x : ℤ // N ≤ x} := analogous to the equivalence between ℕ and {x // x ∉ finset.range N} provided by docs#not_mem_range_equiv.

[Yaël Dillies]

There are many ways to provide it, one of the most general being going through docs#succ_archimedean following the TODO I left at the top of the file.

[Yaël Dillies]

Of course, if you want that concrete equivalence decorated with something else than order properties, ignore my stuff :smile:

[Filippo A. E. Nuccio]

Thanks! I have a proof, but I was just wondering if I was fooling around for nothing. Your link does not work for me, but I'll have a look. Got it!

[Yaël Dillies]

Arf, docs#is_succ_archimedean, sorry

[Yury G. Kudryashov]

I think that we should use explicit formulas for this equivalence.

[Yaël Dillies]

@Filippo A. E. Nuccio, we actually have something very similar already: docs#finset.not_mem_range_equiv. It's only once in mathlib so feel free to make it nicer!

[Filippo A. E. Nuccio]

@Yaël Dillies Yes, thanks! That was the thing I was starting with when I realized by finset was not a finset nat. I already have a generalized version, so I will soon PR something.