Commit 2023-03-17 12:30 75957565
View on Github →chore(data/fintype/fin): add Iio lemmas (#18600)
These are the analogue to the existing Ioi
lemmas in this file.
Iio_last_eq_map
is the dual of Ioi_zero_eq_map
, and Iio_cast_succ
is the dual of Ioi_succ
.
I couldn't find a better home for map_subtype_embedding_univ
.
Note that it is deliberately subtype_embedding
and not coe_embedding
to match the similarly-misnamed fin.map_subtype_embedding_Iio