Commit 2025-03-13 19:08 3c4ebeb4

View on Github →

feat(Interval/Set/Fin): new file (#22452)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Interval/Set/Fin.lean

added theorem Fin.image_addNat_Icc

added theorem Fin.image_addNat_Ici

added theorem Fin.image_addNat_Ico

added theorem Fin.image_addNat_Ioc

added theorem Fin.image_addNat_Ioi

added theorem Fin.image_addNat_Ioo

added theorem Fin.image_cast

added theorem Fin.image_castAdd_Icc

added theorem Fin.image_castAdd_Ici

added theorem Fin.image_castAdd_Ico

added theorem Fin.image_castAdd_Iic

added theorem Fin.image_castAdd_Iio

added theorem Fin.image_castAdd_Ioc

added theorem Fin.image_castAdd_Ioi

added theorem Fin.image_castAdd_Ioo

added theorem Fin.image_castLE_Icc

added theorem Fin.image_castLE_Ico

added theorem Fin.image_castLE_Iic

added theorem Fin.image_castLE_Iio

added theorem Fin.image_castLE_Ioc

added theorem Fin.image_castLE_Ioo

added theorem Fin.image_castSucc_Icc

added theorem Fin.image_castSucc_Ici

added theorem Fin.image_castSucc_Ico

added theorem Fin.image_castSucc_Iic

added theorem Fin.image_castSucc_Iio

added theorem Fin.image_castSucc_Ioc

added theorem Fin.image_castSucc_Ioi

added theorem Fin.image_castSucc_Ioo

added theorem Fin.image_cast_fun

added theorem Fin.image_natAdd_Icc

added theorem Fin.image_natAdd_Ici

added theorem Fin.image_natAdd_Ico

added theorem Fin.image_natAdd_Ioc

added theorem Fin.image_natAdd_Ioi

added theorem Fin.image_natAdd_Ioo

added theorem Fin.image_rev

added theorem Fin.image_rev_fun

added theorem Fin.image_succ_Icc

added theorem Fin.image_succ_Ici

added theorem Fin.image_succ_Ico

added theorem Fin.image_succ_Iic

added theorem Fin.image_succ_Iio

added theorem Fin.image_succ_Ioc

added theorem Fin.image_succ_Ioi

added theorem Fin.image_succ_Ioo

added theorem Fin.image_val_Icc

added theorem Fin.image_val_Ici

added theorem Fin.image_val_Ico

added theorem Fin.image_val_Iic

added theorem Fin.image_val_Iio

added theorem Fin.image_val_Ioc

added theorem Fin.image_val_Ioi

added theorem Fin.image_val_Ioo

added theorem Fin.preimage_addNat_Icc_addNat

added theorem Fin.preimage_addNat_Ici_addNat

added theorem Fin.preimage_addNat_Ico_addNat

added theorem Fin.preimage_addNat_Iic_addNat

added theorem Fin.preimage_addNat_Iio_addNat

added theorem Fin.preimage_addNat_Ioc_addNat

added theorem Fin.preimage_addNat_Ioi_addNat

added theorem Fin.preimage_addNat_Ioo_addNat

added theorem Fin.preimage_castAdd_Icc_castAdd

added theorem Fin.preimage_castAdd_Ici_castAdd

added theorem Fin.preimage_castAdd_Ico_castAdd

added theorem Fin.preimage_castAdd_Iic_castAdd

added theorem Fin.preimage_castAdd_Iio_castAdd

added theorem Fin.preimage_castAdd_Ioc_castAdd

added theorem Fin.preimage_castAdd_Ioi_castAdd

added theorem Fin.preimage_castAdd_Ioo_castAdd

added theorem Fin.preimage_castLE_Icc_castLE

added theorem Fin.preimage_castLE_Ici_castLE

added theorem Fin.preimage_castLE_Ico_castLE

added theorem Fin.preimage_castLE_Iic_castLE

added theorem Fin.preimage_castLE_Iio_castLE

added theorem Fin.preimage_castLE_Ioc_castLE

added theorem Fin.preimage_castLE_Ioi_castLE

added theorem Fin.preimage_castLE_Ioo_castLE

added theorem Fin.preimage_castSucc_Icc_castSucc

added theorem Fin.preimage_castSucc_Ici_castSucc

added theorem Fin.preimage_castSucc_Ico_castSucc

added theorem Fin.preimage_castSucc_Iic_castSucc

added theorem Fin.preimage_castSucc_Iio_castSucc

added theorem Fin.preimage_castSucc_Ioc_castSucc

added theorem Fin.preimage_castSucc_Ioi_castSucc

added theorem Fin.preimage_castSucc_Ioo_castSucc

added theorem Fin.preimage_cast_Icc

added theorem Fin.preimage_cast_Ici

added theorem Fin.preimage_cast_Ico

added theorem Fin.preimage_cast_Iic

added theorem Fin.preimage_cast_Iio

added theorem Fin.preimage_cast_Ioc

added theorem Fin.preimage_cast_Ioi

added theorem Fin.preimage_cast_Ioo

added theorem Fin.preimage_natAdd_Icc_natAdd

added theorem Fin.preimage_natAdd_Ici_natAdd

added theorem Fin.preimage_natAdd_Ico_natAdd

added theorem Fin.preimage_natAdd_Iic_natAdd

added theorem Fin.preimage_natAdd_Iio_natAdd

added theorem Fin.preimage_natAdd_Ioc_natAdd

added theorem Fin.preimage_natAdd_Ioi_natAdd

added theorem Fin.preimage_natAdd_Ioo_natAdd

added theorem Fin.preimage_rev_Icc

added theorem Fin.preimage_rev_Ici

added theorem Fin.preimage_rev_Ico

added theorem Fin.preimage_rev_Iic

added theorem Fin.preimage_rev_Iio

added theorem Fin.preimage_rev_Ioc

added theorem Fin.preimage_rev_Ioi

added theorem Fin.preimage_rev_Ioo

added theorem Fin.preimage_succ_Icc_succ

added theorem Fin.preimage_succ_Ici_succ

added theorem Fin.preimage_succ_Ico_succ

added theorem Fin.preimage_succ_Iic_succ

added theorem Fin.preimage_succ_Iio_succ

added theorem Fin.preimage_succ_Ioc_succ

added theorem Fin.preimage_succ_Ioi_succ

added theorem Fin.preimage_succ_Ioo_succ

added theorem Fin.preimage_val_Icc_val

added theorem Fin.preimage_val_Ici_val

added theorem Fin.preimage_val_Ico_val

added theorem Fin.preimage_val_Iic_val

added theorem Fin.preimage_val_Iio_val

added theorem Fin.preimage_val_Ioc_val

added theorem Fin.preimage_val_Ioi_val

added theorem Fin.preimage_val_Ioo_val

added theorem Fin.range_castAdd

added theorem Fin.range_natAdd

added theorem Fin.range_natAdd_eq_Ici

added theorem Fin.range_natAdd_eq_Ioi

added theorem Fin.range_rev

added theorem Fin.range_val