Commit 2023-08-03 05:30 50ce43f7

View on Github →

feat: add instances for intervals (#5957) Don't mind at all if anyone would like to push refactors or golfs. My main requirement from this PR is that

import Mathlib
example : WellFoundedLT { x : ℕ // x ≤ 37 }ᵒᵈ := inferInstance

works out of the box.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/PNat/Interval.lean

Modified Mathlib/Data/Set/Function.lean

added theorem Set.injOn_subtype_val

Created Mathlib/Data/Set/Intervals/Image.lean

added theorem Monotone.image_Icc_subset

added theorem Monotone.image_Ici_subset

added theorem Monotone.image_Iic_subset

added theorem Monotone.mapsTo_Icc

added theorem Monotone.mapsTo_Ici

added theorem Monotone.mapsTo_Iic

added theorem Set.image_subtype_val_Icc_subset

added theorem Set.image_subtype_val_Ici_subset

added theorem Set.image_subtype_val_Ico_subset

added theorem Set.image_subtype_val_Iic_subset

added theorem Set.image_subtype_val_Iio_subset

added theorem Set.image_subtype_val_Ioc_subset

added theorem Set.image_subtype_val_Ioi_subset

added theorem Set.image_subtype_val_Ioo_subset

added theorem StrictMono.imageIco_subset

added theorem StrictMono.imageIoc_subset

added theorem StrictMono.image_Iio_subset

added theorem StrictMono.image_Ioi_subset

added theorem StrictMono.image_Ioo_subset

added theorem StrictMono.mapsTo_Ico

added theorem StrictMono.mapsTo_Iio

added theorem StrictMono.mapsTo_Ioc

added theorem StrictMono.mapsTo_Ioi

added theorem StrictMono.mapsTo_Ioo

Modified Mathlib/NumberTheory/NumberField/Units.lean

Modified Mathlib/Order/LocallyFinite.lean