Fin

📁 Source: Mathlib/Order/Interval/Set/Fin.lean

Statistics

Metric	Count
Definitions	0
Theorems image_addNat_Icc, image_addNat_Ici, image_addNat_Ico, image_addNat_Ioc, image_addNat_Ioi, image_addNat_Ioo, image_addNat_uIcc, image_addNat_uIoc, image_addNat_uIoo, image_cast, image_castAdd_Icc, image_castAdd_Ici, image_castAdd_Ico, image_castAdd_Iic, image_castAdd_Iio, image_castAdd_Ioc, image_castAdd_Ioi, image_castAdd_Ioo, image_castAdd_uIcc, image_castAdd_uIoc, image_castAdd_uIoo, image_castLE_Icc, image_castLE_Ico, image_castLE_Iic, image_castLE_Iio, image_castLE_Ioc, image_castLE_Ioo, image_castLE_uIcc, image_castLE_uIoc, image_castLE_uIoo, image_castSucc_Icc, image_castSucc_Ici, image_castSucc_Ico, image_castSucc_Iic, image_castSucc_Iio, image_castSucc_Ioc, image_castSucc_Ioi, image_castSucc_Ioo, image_castSucc_uIcc, image_castSucc_uIoc, image_castSucc_uIoo, image_cast_fun, image_natAdd_Icc, image_natAdd_Ici, image_natAdd_Ico, image_natAdd_Ioc, image_natAdd_Ioi, image_natAdd_Ioo, image_natAdd_uIcc, image_natAdd_uIoc, image_natAdd_uIoo, image_rev, image_rev_fun, image_succ_Icc, image_succ_Ici, image_succ_Ico, image_succ_Iic, image_succ_Iio, image_succ_Ioc, image_succ_Ioi, image_succ_Ioo, image_succ_uIcc, image_succ_uIoc, image_succ_uIoo, image_val_Icc, image_val_Ici, image_val_Ico, image_val_Iic, image_val_Iio, image_val_Ioc, image_val_Ioi, image_val_Ioo, image_val_uIcc, image_val_uIoc, image_val_uIoo, preimage_addNat_Icc_addNat, preimage_addNat_Ici_addNat, preimage_addNat_Ico_addNat, preimage_addNat_Iic_addNat, preimage_addNat_Iio_addNat, preimage_addNat_Ioc_addNat, preimage_addNat_Ioi_addNat, preimage_addNat_Ioo_addNat, preimage_addNat_uIcc_addNat, preimage_addNat_uIoc_addNat, preimage_addNat_uIoo_addNat, preimage_castAdd_Icc_castAdd, preimage_castAdd_Ici_castAdd, preimage_castAdd_Ico_castAdd, preimage_castAdd_Iic_castAdd, preimage_castAdd_Iio_castAdd, preimage_castAdd_Ioc_castAdd, preimage_castAdd_Ioi_castAdd, preimage_castAdd_Ioo_castAdd, preimage_castAdd_uIcc_castAdd, preimage_castAdd_uIoc_castAdd, preimage_castAdd_uIoo_castAdd, preimage_castLE_Icc_castLE, preimage_castLE_Ici_castLE, preimage_castLE_Ico_castLE, preimage_castLE_Iic_castLE, preimage_castLE_Iio_castLE, preimage_castLE_Ioc_castLE, preimage_castLE_Ioi_castLE, preimage_castLE_Ioo_castLE, preimage_castLE_uIcc_castLE, preimage_castLE_uIoc_castLE, preimage_castLE_uIoo_castLE, preimage_castSucc_Icc_castSucc, preimage_castSucc_Ici_castSucc, preimage_castSucc_Ico_castSucc, preimage_castSucc_Iic_castSucc, preimage_castSucc_Iio_castSucc, preimage_castSucc_Ioc_castSucc, preimage_castSucc_Ioi_castSucc, preimage_castSucc_Ioo_castSucc, preimage_castSucc_uIcc_castSucc, preimage_castSucc_uIoc_castSucc, preimage_castSucc_uIoo_castSucc, preimage_cast_Icc, preimage_cast_Ici, preimage_cast_Ico, preimage_cast_Iic, preimage_cast_Iio, preimage_cast_Ioc, preimage_cast_Ioi, preimage_cast_Ioo, preimage_cast_uIcc, preimage_cast_uIoc, preimage_cast_uIoo, preimage_natAdd_Icc_natAdd, preimage_natAdd_Ici_natAdd, preimage_natAdd_Ico_natAdd, preimage_natAdd_Iic_natAdd, preimage_natAdd_Iio_natAdd, preimage_natAdd_Ioc_natAdd, preimage_natAdd_Ioi_natAdd, preimage_natAdd_Ioo_natAdd, preimage_natAdd_uIcc_natAdd, preimage_natAdd_uIoc_natAdd, preimage_natAdd_uIoo_natAdd, preimage_rev_Icc, preimage_rev_Ici, preimage_rev_Ico, preimage_rev_Iic, preimage_rev_Iio, preimage_rev_Ioc, preimage_rev_Ioi, preimage_rev_Ioo, preimage_rev_uIcc, preimage_rev_uIoo, preimage_succ_Icc_succ, preimage_succ_Ici_succ, preimage_succ_Ico_succ, preimage_succ_Iic_succ, preimage_succ_Iio_succ, preimage_succ_Ioc_succ, preimage_succ_Ioi_succ, preimage_succ_Ioo_succ, preimage_succ_uIcc_succ, preimage_succ_uIoc_succ, preimage_succ_uIoo_succ, preimage_val_Icc_val, preimage_val_Ici_val, preimage_val_Ico_val, preimage_val_Iic_val, preimage_val_Iio_val, preimage_val_Ioc_val, preimage_val_Ioi_val, preimage_val_Ioo_val, preimage_val_uIcc_val, preimage_val_uIoc_val, preimage_val_uIoo_val, range_castAdd, range_natAdd, range_natAdd_eq_Ici, range_natAdd_eq_Ioi, range_rev, range_val	179
Total	179

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_addNat_Icc 📖	mathematical	—	Set.image Set.Icc PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Icc_addNat Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Icc_subset_Ici_self Set.image_subset_range image_addNat_Ici
image_addNat_Ici 📖	mathematical	—	Set.image Set.Ici PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ici_addNat Set.image_preimage_eq_of_subset
image_addNat_Ico 📖	mathematical	—	Set.image Set.Ico PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ico_addNat Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ico_subset_Ici_self Set.image_subset_range image_addNat_Ici
image_addNat_Ioc 📖	mathematical	—	Set.image Set.Ioc PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ioc_addNat Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ioc_subset_Ioi_self Set.image_subset_range image_addNat_Ioi
image_addNat_Ioi 📖	mathematical	—	Set.image Set.Ioi PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ioi_addNat Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ioi_subset_Ici_self Set.image_subset_range image_addNat_Ici
image_addNat_Ioo 📖	mathematical	—	Set.image Set.Ioo PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ioo_addNat Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ioo_subset_Ioi_self Set.image_subset_range image_addNat_Ioi
image_addNat_uIcc 📖	mathematical	—	Set.image Set.uIcc instLattice	—	image_addNat_Icc Monotone.map_min StrictMono.monotone strictMono_addNat Monotone.map_max
image_addNat_uIoc 📖	mathematical	—	Set.image Set.uIoc instLinearOrder	—	image_addNat_Ioc Monotone.map_min StrictMono.monotone strictMono_addNat Monotone.map_max
image_addNat_uIoo 📖	mathematical	—	Set.image Set.uIoo instLinearOrder	—	image_addNat_Ioo Monotone.map_min StrictMono.monotone strictMono_addNat Monotone.map_max
image_cast 📖	mathematical	—	Set.image Set.preimage	—	Equiv.image_eq_preimage_symm
image_castAdd_Icc 📖	mathematical	—	Set.image Set.Icc PartialOrder.toPreorder instPartialOrder	—	image_castLE_Icc
image_castAdd_Ici 📖	mathematical	—	Set.image Set.Ici PartialOrder.toPreorder instPartialOrder Set.Ico	—	Function.Injective.image_injective val_injective Set.image_congr image_val_Ici image_val_Ico
image_castAdd_Ico 📖	mathematical	—	Set.image Set.Ico PartialOrder.toPreorder instPartialOrder	—	image_castLE_Ico
image_castAdd_Iic 📖	mathematical	—	Set.image Set.Iic PartialOrder.toPreorder instPartialOrder	—	image_castLE_Iic
image_castAdd_Iio 📖	mathematical	—	Set.image Set.Iio PartialOrder.toPreorder instPartialOrder	—	image_castLE_Iio
image_castAdd_Ioc 📖	mathematical	—	Set.image Set.Ioc PartialOrder.toPreorder instPartialOrder	—	image_castLE_Ioc
image_castAdd_Ioi 📖	mathematical	—	Set.image Set.Ioi PartialOrder.toPreorder instPartialOrder Set.Ioo	—	Function.Injective.image_injective val_injective Set.image_congr image_val_Ioi image_val_Ioo
image_castAdd_Ioo 📖	mathematical	—	Set.image Set.Ioo PartialOrder.toPreorder instPartialOrder	—	image_castLE_Ioo
image_castAdd_uIcc 📖	mathematical	—	Set.image Set.uIcc instLattice	—	image_castLE_uIcc
image_castAdd_uIoc 📖	mathematical	—	Set.image Set.uIoc instLinearOrder	—	image_castLE_uIoc
image_castAdd_uIoo 📖	mathematical	—	Set.image Set.uIoo instLinearOrder	—	image_castLE_uIoo
image_castLE_Icc 📖	mathematical	—	Set.image Set.Icc PartialOrder.toPreorder instPartialOrder	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_Icc
image_castLE_Ico 📖	mathematical	—	Set.image Set.Ico PartialOrder.toPreorder instPartialOrder	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_Ico
image_castLE_Iic 📖	mathematical	—	Set.image Set.Iic PartialOrder.toPreorder instPartialOrder	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_Iic
image_castLE_Iio 📖	mathematical	—	Set.image Set.Iio PartialOrder.toPreorder instPartialOrder	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_Iio
image_castLE_Ioc 📖	mathematical	—	Set.image Set.Ioc PartialOrder.toPreorder instPartialOrder	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_Ioc
image_castLE_Ioo 📖	mathematical	—	Set.image Set.Ioo PartialOrder.toPreorder instPartialOrder	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_Ioo
image_castLE_uIcc 📖	mathematical	—	Set.image Set.uIcc instLattice	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_uIcc
image_castLE_uIoc 📖	mathematical	—	Set.image Set.uIoc instLinearOrder	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_uIoc
image_castLE_uIoo 📖	mathematical	—	Set.image Set.uIoo instLinearOrder	—	Function.Injective.image_injective val_injective Set.image_image Set.image_congr image_val_uIoo
image_castSucc_Icc 📖	mathematical	—	Set.image Set.Icc PartialOrder.toPreorder instPartialOrder	—	image_castAdd_Icc
image_castSucc_Ici 📖	mathematical	—	Set.image Set.Ici PartialOrder.toPreorder instPartialOrder Set.Ico	—	image_castAdd_Ici
image_castSucc_Ico 📖	mathematical	—	Set.image Set.Ico PartialOrder.toPreorder instPartialOrder	—	image_castAdd_Ico
image_castSucc_Iic 📖	mathematical	—	Set.image Set.Iic PartialOrder.toPreorder instPartialOrder	—	image_castAdd_Iic
image_castSucc_Iio 📖	mathematical	—	Set.image Set.Iio PartialOrder.toPreorder instPartialOrder	—	image_castAdd_Iio
image_castSucc_Ioc 📖	mathematical	—	Set.image Set.Ioc PartialOrder.toPreorder instPartialOrder	—	image_castAdd_Ioc
image_castSucc_Ioi 📖	mathematical	—	Set.image Set.Ioi PartialOrder.toPreorder instPartialOrder Set.Ioo	—	image_castAdd_Ioi
image_castSucc_Ioo 📖	mathematical	—	Set.image Set.Ioo PartialOrder.toPreorder instPartialOrder	—	image_castAdd_Ioo
image_castSucc_uIcc 📖	mathematical	—	Set.image Set.uIcc instLattice	—	image_castAdd_uIcc
image_castSucc_uIoc 📖	mathematical	—	Set.image Set.uIoc instLinearOrder	—	image_castAdd_uIoc
image_castSucc_uIoo 📖	mathematical	—	Set.image Set.uIoo instLinearOrder	—	image_castAdd_uIoo
image_cast_fun 📖	mathematical	—	Set.image Set.preimage	—	image_cast
image_natAdd_Icc 📖	mathematical	—	Set.image Set.Icc PartialOrder.toPreorder instPartialOrder	—	preimage_natAdd_Icc_natAdd Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Icc_subset_Ici_self Set.image_subset_range image_natAdd_Ici
image_natAdd_Ici 📖	mathematical	—	Set.image Set.Ici PartialOrder.toPreorder instPartialOrder	—	preimage_natAdd_Ici_natAdd Set.image_preimage_eq_of_subset range_natAdd
image_natAdd_Ico 📖	mathematical	—	Set.image Set.Ico PartialOrder.toPreorder instPartialOrder	—	preimage_natAdd_Ico_natAdd Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ico_subset_Ici_self Set.image_subset_range image_natAdd_Ici
image_natAdd_Ioc 📖	mathematical	—	Set.image Set.Ioc PartialOrder.toPreorder instPartialOrder	—	preimage_natAdd_Ioc_natAdd Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ioc_subset_Ioi_self Set.image_subset_range image_natAdd_Ioi
image_natAdd_Ioi 📖	mathematical	—	Set.image Set.Ioi PartialOrder.toPreorder instPartialOrder	—	preimage_natAdd_Ioi_natAdd Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ioi_subset_Ici_self Set.image_subset_range image_natAdd_Ici
image_natAdd_Ioo 📖	mathematical	—	Set.image Set.Ioo PartialOrder.toPreorder instPartialOrder	—	preimage_natAdd_Ioo_natAdd Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ioo_subset_Ioi_self Set.image_subset_range image_natAdd_Ioi
image_natAdd_uIcc 📖	mathematical	—	Set.image Set.uIcc instLattice	—	image_natAdd_Icc Monotone.map_min StrictMono.monotone strictMono_natAdd Monotone.map_max
image_natAdd_uIoc 📖	mathematical	—	Set.image Set.uIoc instLinearOrder	—	image_natAdd_Ioc Monotone.map_min StrictMono.monotone strictMono_natAdd Monotone.map_max
image_natAdd_uIoo 📖	mathematical	—	Set.image Set.uIoo instLinearOrder	—	image_natAdd_Ioo Monotone.map_min StrictMono.monotone strictMono_natAdd Monotone.map_max
image_rev 📖	mathematical	—	Set.image Set.preimage	—	Equiv.image_eq_preimage_symm
image_rev_fun 📖	mathematical	—	Set.image Set.preimage	—	image_rev
image_succ_Icc 📖	mathematical	—	Set.image Set.Icc PartialOrder.toPreorder instPartialOrder	—	image_addNat_Icc
image_succ_Ici 📖	mathematical	—	Set.image Set.Ici PartialOrder.toPreorder instPartialOrder	—	image_addNat_Ici
image_succ_Ico 📖	mathematical	—	Set.image Set.Ico PartialOrder.toPreorder instPartialOrder	—	image_addNat_Ico
image_succ_Iic 📖	mathematical	—	Set.image Set.Iic PartialOrder.toPreorder instPartialOrder Set.Ioc	—	Set.Subset.antisymm Set.image_subset_iff exists_succ_eq_of_ne_zero LT.lt.ne' Set.mem_image_of_mem
image_succ_Iio 📖	mathematical	—	Set.image Set.Iio PartialOrder.toPreorder instPartialOrder Set.Ioo	—	Set.Subset.antisymm Set.image_subset_iff exists_succ_eq_of_ne_zero LT.lt.ne' Set.mem_image_of_mem
image_succ_Ioc 📖	mathematical	—	Set.image Set.Ioc PartialOrder.toPreorder instPartialOrder	—	image_addNat_Ioc
image_succ_Ioi 📖	mathematical	—	Set.image Set.Ioi PartialOrder.toPreorder instPartialOrder	—	image_addNat_Ioi
image_succ_Ioo 📖	mathematical	—	Set.image Set.Ioo PartialOrder.toPreorder instPartialOrder	—	image_addNat_Ioo
image_succ_uIcc 📖	mathematical	—	Set.image Set.uIcc instLattice	—	image_addNat_uIcc
image_succ_uIoc 📖	mathematical	—	Set.image Set.uIoc instLinearOrder	—	image_addNat_uIoc
image_succ_uIoo 📖	mathematical	—	Set.image Set.uIoo instLinearOrder	—	image_addNat_uIoo
image_val_Icc 📖	mathematical	—	Set.image Set.Icc PartialOrder.toPreorder instPartialOrder Nat.instPreorder	—	preimage_val_Icc_val Set.image_preimage_eq_inter_range range_val Set.inter_eq_left LE.le.trans_lt
image_val_Ici 📖	mathematical	—	Set.image Set.Ici PartialOrder.toPreorder instPartialOrder Set.Ico Nat.instPreorder	—	preimage_val_Ici_val Set.image_preimage_eq_inter_range range_val Set.Ici_inter_Iio
image_val_Ico 📖	mathematical	—	Set.image Set.Ico PartialOrder.toPreorder instPartialOrder Nat.instPreorder	—	preimage_val_Ico_val Set.image_preimage_eq_inter_range range_val Set.inter_eq_left LT.lt.trans
image_val_Iic 📖	mathematical	—	Set.image Set.Iic PartialOrder.toPreorder instPartialOrder Nat.instPreorder	—	preimage_val_Iic_val Set.image_preimage_eq_of_subset range_val
image_val_Iio 📖	mathematical	—	Set.image Set.Iio PartialOrder.toPreorder instPartialOrder Nat.instPreorder	—	preimage_val_Iio_val Set.image_preimage_eq_inter_range range_val Set.inter_eq_left Set.Iio_subset_Iio LT.lt.le
image_val_Ioc 📖	mathematical	—	Set.image Set.Ioc PartialOrder.toPreorder instPartialOrder Nat.instPreorder	—	preimage_val_Ioc_val Set.image_preimage_eq_inter_range range_val Set.inter_eq_left LE.le.trans_lt
image_val_Ioi 📖	mathematical	—	Set.image Set.Ioi PartialOrder.toPreorder instPartialOrder Set.Ioo Nat.instPreorder	—	preimage_val_Ioi_val Set.image_preimage_eq_inter_range range_val Set.Ioi_inter_Iio
image_val_Ioo 📖	mathematical	—	Set.image Set.Ioo PartialOrder.toPreorder instPartialOrder Nat.instPreorder	—	preimage_val_Ioo_val Set.image_preimage_eq_inter_range range_val Set.inter_eq_left LT.lt.trans
image_val_uIcc 📖	mathematical	—	Set.image Set.uIcc instLattice DistribLattice.toLattice instDistribLatticeNat	—	image_val_Icc
image_val_uIoc 📖	mathematical	—	Set.image Set.uIoc instLinearOrder Nat.instLinearOrder	—	image_val_Ioc
image_val_uIoo 📖	mathematical	—	Set.image Set.uIoo instLinearOrder Nat.instLinearOrder	—	image_val_Ioo
preimage_addNat_Icc_addNat 📖	mathematical	—	Set.preimage Set.Icc PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_addNat_Ici_addNat 📖	mathematical	—	Set.preimage Set.Ici PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_addNat_Ico_addNat 📖	mathematical	—	Set.preimage Set.Ico PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_addNat_Iic_addNat 📖	mathematical	—	Set.preimage Set.Iic PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_addNat_Iio_addNat 📖	mathematical	—	Set.preimage Set.Iio PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_addNat_Ioc_addNat 📖	mathematical	—	Set.preimage Set.Ioc PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_addNat_Ioi_addNat 📖	mathematical	—	Set.preimage Set.Ioi PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_addNat_Ioo_addNat 📖	mathematical	—	Set.preimage Set.Ioo PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_addNat_uIcc_addNat 📖	mathematical	—	Set.preimage Set.uIcc instLattice	—	Monotone.map_min StrictMono.monotone strictMono_addNat Monotone.map_max preimage_addNat_Icc_addNat
preimage_addNat_uIoc_addNat 📖	mathematical	—	Set.preimage Set.uIoc instLinearOrder	—	Monotone.map_min StrictMono.monotone strictMono_addNat Monotone.map_max preimage_addNat_Ioc_addNat
preimage_addNat_uIoo_addNat 📖	mathematical	—	Set.preimage Set.uIoo instLinearOrder	—	Monotone.map_min StrictMono.monotone strictMono_addNat Monotone.map_max preimage_addNat_Ioo_addNat
preimage_castAdd_Icc_castAdd 📖	mathematical	—	Set.preimage Set.Icc PartialOrder.toPreorder instPartialOrder	—	—
preimage_castAdd_Ici_castAdd 📖	mathematical	—	Set.preimage Set.Ici PartialOrder.toPreorder instPartialOrder	—	—
preimage_castAdd_Ico_castAdd 📖	mathematical	—	Set.preimage Set.Ico PartialOrder.toPreorder instPartialOrder	—	—
preimage_castAdd_Iic_castAdd 📖	mathematical	—	Set.preimage Set.Iic PartialOrder.toPreorder instPartialOrder	—	—
preimage_castAdd_Iio_castAdd 📖	mathematical	—	Set.preimage Set.Iio PartialOrder.toPreorder instPartialOrder	—	—
preimage_castAdd_Ioc_castAdd 📖	mathematical	—	Set.preimage Set.Ioc PartialOrder.toPreorder instPartialOrder	—	—
preimage_castAdd_Ioi_castAdd 📖	mathematical	—	Set.preimage Set.Ioi PartialOrder.toPreorder instPartialOrder	—	—
preimage_castAdd_Ioo_castAdd 📖	mathematical	—	Set.preimage Set.Ioo PartialOrder.toPreorder instPartialOrder	—	—
preimage_castAdd_uIcc_castAdd 📖	mathematical	—	Set.preimage Set.uIcc instLattice	—	—
preimage_castAdd_uIoc_castAdd 📖	mathematical	—	Set.preimage Set.uIoc instLinearOrder	—	—
preimage_castAdd_uIoo_castAdd 📖	mathematical	—	Set.preimage Set.uIoo instLinearOrder	—	—
preimage_castLE_Icc_castLE 📖	mathematical	—	Set.preimage Set.Icc PartialOrder.toPreorder instPartialOrder	—	—
preimage_castLE_Ici_castLE 📖	mathematical	—	Set.preimage Set.Ici PartialOrder.toPreorder instPartialOrder	—	—
preimage_castLE_Ico_castLE 📖	mathematical	—	Set.preimage Set.Ico PartialOrder.toPreorder instPartialOrder	—	—
preimage_castLE_Iic_castLE 📖	mathematical	—	Set.preimage Set.Iic PartialOrder.toPreorder instPartialOrder	—	—
preimage_castLE_Iio_castLE 📖	mathematical	—	Set.preimage Set.Iio PartialOrder.toPreorder instPartialOrder	—	—
preimage_castLE_Ioc_castLE 📖	mathematical	—	Set.preimage Set.Ioc PartialOrder.toPreorder instPartialOrder	—	—
preimage_castLE_Ioi_castLE 📖	mathematical	—	Set.preimage Set.Ioi PartialOrder.toPreorder instPartialOrder	—	—
preimage_castLE_Ioo_castLE 📖	mathematical	—	Set.preimage Set.Ioo PartialOrder.toPreorder instPartialOrder	—	—
preimage_castLE_uIcc_castLE 📖	mathematical	—	Set.preimage Set.uIcc instLattice	—	—
preimage_castLE_uIoc_castLE 📖	mathematical	—	Set.preimage Set.uIoc instLinearOrder	—	—
preimage_castLE_uIoo_castLE 📖	mathematical	—	Set.preimage Set.uIoo instLinearOrder	—	—
preimage_castSucc_Icc_castSucc 📖	mathematical	—	Set.preimage Set.Icc PartialOrder.toPreorder instPartialOrder	—	—
preimage_castSucc_Ici_castSucc 📖	mathematical	—	Set.preimage Set.Ici PartialOrder.toPreorder instPartialOrder	—	—
preimage_castSucc_Ico_castSucc 📖	mathematical	—	Set.preimage Set.Ico PartialOrder.toPreorder instPartialOrder	—	—
preimage_castSucc_Iic_castSucc 📖	mathematical	—	Set.preimage Set.Iic PartialOrder.toPreorder instPartialOrder	—	—
preimage_castSucc_Iio_castSucc 📖	mathematical	—	Set.preimage Set.Iio PartialOrder.toPreorder instPartialOrder	—	—
preimage_castSucc_Ioc_castSucc 📖	mathematical	—	Set.preimage Set.Ioc PartialOrder.toPreorder instPartialOrder	—	—
preimage_castSucc_Ioi_castSucc 📖	mathematical	—	Set.preimage Set.Ioi PartialOrder.toPreorder instPartialOrder	—	—
preimage_castSucc_Ioo_castSucc 📖	mathematical	—	Set.preimage Set.Ioo PartialOrder.toPreorder instPartialOrder	—	—
preimage_castSucc_uIcc_castSucc 📖	mathematical	—	Set.preimage Set.uIcc instLattice	—	—
preimage_castSucc_uIoc_castSucc 📖	mathematical	—	Set.preimage Set.uIoc instLinearOrder	—	—
preimage_castSucc_uIoo_castSucc 📖	mathematical	—	Set.preimage Set.uIoo instLinearOrder	—	—
preimage_cast_Icc 📖	mathematical	—	Set.preimage Set.Icc PartialOrder.toPreorder instPartialOrder	—	—
preimage_cast_Ici 📖	mathematical	—	Set.preimage Set.Ici PartialOrder.toPreorder instPartialOrder	—	—
preimage_cast_Ico 📖	mathematical	—	Set.preimage Set.Ico PartialOrder.toPreorder instPartialOrder	—	—
preimage_cast_Iic 📖	mathematical	—	Set.preimage Set.Iic PartialOrder.toPreorder instPartialOrder	—	—
preimage_cast_Iio 📖	mathematical	—	Set.preimage Set.Iio PartialOrder.toPreorder instPartialOrder	—	—
preimage_cast_Ioc 📖	mathematical	—	Set.preimage Set.Ioc PartialOrder.toPreorder instPartialOrder	—	—
preimage_cast_Ioi 📖	mathematical	—	Set.preimage Set.Ioi PartialOrder.toPreorder instPartialOrder	—	—
preimage_cast_Ioo 📖	mathematical	—	Set.preimage Set.Ioo PartialOrder.toPreorder instPartialOrder	—	—
preimage_cast_uIcc 📖	mathematical	—	Set.preimage Set.uIcc instLattice	—	—
preimage_cast_uIoc 📖	mathematical	—	Set.preimage Set.uIoc instLinearOrder	—	—
preimage_cast_uIoo 📖	mathematical	—	Set.preimage Set.uIoo instLinearOrder	—	—
preimage_natAdd_Icc_natAdd 📖	mathematical	—	Set.preimage Set.Icc PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_natAdd_Ici_natAdd 📖	mathematical	—	Set.preimage Set.Ici PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_natAdd_Ico_natAdd 📖	mathematical	—	Set.preimage Set.Ico PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_natAdd_Iic_natAdd 📖	mathematical	—	Set.preimage Set.Iic PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_natAdd_Iio_natAdd 📖	mathematical	—	Set.preimage Set.Iio PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_natAdd_Ioc_natAdd 📖	mathematical	—	Set.preimage Set.Ioc PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_natAdd_Ioi_natAdd 📖	mathematical	—	Set.preimage Set.Ioi PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_natAdd_Ioo_natAdd 📖	mathematical	—	Set.preimage Set.Ioo PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_natAdd_uIcc_natAdd 📖	mathematical	—	Set.preimage Set.uIcc instLattice	—	Monotone.map_min StrictMono.monotone strictMono_natAdd Monotone.map_max preimage_natAdd_Icc_natAdd
preimage_natAdd_uIoc_natAdd 📖	mathematical	—	Set.preimage Set.uIoc instLinearOrder	—	Monotone.map_min StrictMono.monotone strictMono_natAdd Monotone.map_max preimage_natAdd_Ioc_natAdd
preimage_natAdd_uIoo_natAdd 📖	mathematical	—	Set.preimage Set.uIoo instLinearOrder	—	Monotone.map_min StrictMono.monotone strictMono_natAdd Monotone.map_max preimage_natAdd_Ioo_natAdd
preimage_rev_Icc 📖	mathematical	—	Set.preimage Set.Icc PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_rev_Ici 📖	mathematical	—	Set.preimage Set.Ici PartialOrder.toPreorder instPartialOrder Set.Iic	—	Set.ext
preimage_rev_Ico 📖	mathematical	—	Set.preimage Set.Ico PartialOrder.toPreorder instPartialOrder Set.Ioc	—	Set.ext
preimage_rev_Iic 📖	mathematical	—	Set.preimage Set.Iic PartialOrder.toPreorder instPartialOrder Set.Ici	—	Set.ext
preimage_rev_Iio 📖	mathematical	—	Set.preimage Set.Iio PartialOrder.toPreorder instPartialOrder Set.Ioi	—	Set.ext
preimage_rev_Ioc 📖	mathematical	—	Set.preimage Set.Ioc PartialOrder.toPreorder instPartialOrder Set.Ico	—	Set.ext
preimage_rev_Ioi 📖	mathematical	—	Set.preimage Set.Ioi PartialOrder.toPreorder instPartialOrder Set.Iio	—	Set.ext
preimage_rev_Ioo 📖	mathematical	—	Set.preimage Set.Ioo PartialOrder.toPreorder instPartialOrder	—	Set.ext
preimage_rev_uIcc 📖	mathematical	—	Set.preimage Set.uIcc instLattice	—	preimage_rev_Icc Antitone.map_max rev_anti Antitone.map_min
preimage_rev_uIoo 📖	mathematical	—	Set.preimage Set.uIoo instLinearOrder	—	preimage_rev_Ioo Antitone.map_max rev_anti Antitone.map_min
preimage_succ_Icc_succ 📖	mathematical	—	Set.preimage Set.Icc PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Icc_addNat
preimage_succ_Ici_succ 📖	mathematical	—	Set.preimage Set.Ici PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ici_addNat
preimage_succ_Ico_succ 📖	mathematical	—	Set.preimage Set.Ico PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ico_addNat
preimage_succ_Iic_succ 📖	mathematical	—	Set.preimage Set.Iic PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Iic_addNat
preimage_succ_Iio_succ 📖	mathematical	—	Set.preimage Set.Iio PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Iio_addNat
preimage_succ_Ioc_succ 📖	mathematical	—	Set.preimage Set.Ioc PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ioc_addNat
preimage_succ_Ioi_succ 📖	mathematical	—	Set.preimage Set.Ioi PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ioi_addNat
preimage_succ_Ioo_succ 📖	mathematical	—	Set.preimage Set.Ioo PartialOrder.toPreorder instPartialOrder	—	preimage_addNat_Ioo_addNat
preimage_succ_uIcc_succ 📖	mathematical	—	Set.preimage Set.uIcc instLattice	—	preimage_addNat_uIcc_addNat
preimage_succ_uIoc_succ 📖	mathematical	—	Set.preimage Set.uIoc instLinearOrder	—	preimage_addNat_uIoc_addNat
preimage_succ_uIoo_succ 📖	mathematical	—	Set.preimage Set.uIoo instLinearOrder	—	preimage_addNat_uIoo_addNat
preimage_val_Icc_val 📖	mathematical	—	Set.preimage Set.Icc Nat.instPreorder PartialOrder.toPreorder instPartialOrder	—	—
preimage_val_Ici_val 📖	mathematical	—	Set.preimage Set.Ici Nat.instPreorder PartialOrder.toPreorder instPartialOrder	—	—
preimage_val_Ico_val 📖	mathematical	—	Set.preimage Set.Ico Nat.instPreorder PartialOrder.toPreorder instPartialOrder	—	—
preimage_val_Iic_val 📖	mathematical	—	Set.preimage Set.Iic Nat.instPreorder PartialOrder.toPreorder instPartialOrder	—	—
preimage_val_Iio_val 📖	mathematical	—	Set.preimage Set.Iio Nat.instPreorder PartialOrder.toPreorder instPartialOrder	—	—
preimage_val_Ioc_val 📖	mathematical	—	Set.preimage Set.Ioc Nat.instPreorder PartialOrder.toPreorder instPartialOrder	—	—
preimage_val_Ioi_val 📖	mathematical	—	Set.preimage Set.Ioi Nat.instPreorder PartialOrder.toPreorder instPartialOrder	—	—
preimage_val_Ioo_val 📖	mathematical	—	Set.preimage Set.Ioo Nat.instPreorder PartialOrder.toPreorder instPartialOrder	—	—
preimage_val_uIcc_val 📖	mathematical	—	Set.preimage Set.uIcc DistribLattice.toLattice instDistribLatticeNat instLattice	—	—
preimage_val_uIoc_val 📖	mathematical	—	Set.preimage Set.uIoc Nat.instLinearOrder instLinearOrder	—	—
preimage_val_uIoo_val 📖	mathematical	—	Set.preimage Set.uIoo Nat.instLinearOrder instLinearOrder	—	—
range_castAdd 📖	mathematical	—	Set.range Set.Iio PartialOrder.toPreorder instPartialOrder	—	Function.Injective.image_injective val_injective range_val image_val_Iio
range_natAdd 📖	mathematical	—	Set.range setOf	—	Set.ext
range_natAdd_eq_Ici 📖	mathematical	—	Set.range Set.Ici PartialOrder.toPreorder instPartialOrder	—	range_natAdd
range_natAdd_eq_Ioi 📖	mathematical	—	Set.range Set.Ioi PartialOrder.toPreorder instPartialOrder Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	Set.ext range_natAdd
range_rev 📖	mathematical	—	Set.range Set.univ	—	Function.Surjective.range_eq rev_surjective
range_val 📖	mathematical	—	Set.range Set.Iio Nat.instPreorder	—	Set.ext

---

← Back to Index