Image

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

Statistics

Metric	Count
Definitions	0
Theorems `image_Icc_subset`, `image_Ici_subset`, `image_Iic_subset`, `mapsTo_Icc`, `mapsTo_Ici`, `mapsTo_Iic`, `image_Icc_subset`, `image_Ici_subset`, `image_Iic_subset`, `mapsTo_Icc`, `mapsTo_Ici`, `mapsTo_Iic`, `image_Icc_subset`, `image_Ici_subset`, `image_Iic_subset`, `mapsTo_Icc`, `mapsTo_Ici`, `mapsTo_Iic`, `image_Icc_subset`, `image_Ici_subset`, `image_Iic_subset`, `mapsTo_Icc`, `mapsTo_Ici`, `mapsTo_Iic`, `image_subtype_val_Icc_Ici`, `image_subtype_val_Icc_Iic`, `image_subtype_val_Icc_Iio`, `image_subtype_val_Icc_Ioi`, `image_subtype_val_Icc_subset`, `image_subtype_val_Ici_Ici`, `image_subtype_val_Ici_Iic`, `image_subtype_val_Ici_Iio`, `image_subtype_val_Ici_Ioi`, `image_subtype_val_Ici_subset`, `image_subtype_val_Ico_Ici`, `image_subtype_val_Ico_Iic`, `image_subtype_val_Ico_Iio`, `image_subtype_val_Ico_Ioi`, `image_subtype_val_Ico_subset`, `image_subtype_val_Iic_Ici`, `image_subtype_val_Iic_Iic`, `image_subtype_val_Iic_Iio`, `image_subtype_val_Iic_Ioi`, `image_subtype_val_Iic_subset`, `image_subtype_val_Iio_Ici`, `image_subtype_val_Iio_Iic`, `image_subtype_val_Iio_Iio`, `image_subtype_val_Iio_Ioi`, `image_subtype_val_Iio_subset`, `image_subtype_val_Ioc_Ici`, `image_subtype_val_Ioc_Iic`, `image_subtype_val_Ioc_Iio`, `image_subtype_val_Ioc_Ioi`, `image_subtype_val_Ioc_subset`, `image_subtype_val_Ioi_Ici`, `image_subtype_val_Ioi_Iic`, `image_subtype_val_Ioi_Iio`, `image_subtype_val_Ioi_Ioi`, `image_subtype_val_Ioi_subset`, `image_subtype_val_Ioo_Ici`, `image_subtype_val_Ioo_Iic`, `image_subtype_val_Ioo_Iio`, `image_subtype_val_Ioo_Ioi`, `image_subtype_val_Ioo_subset`, `preimage_subtype_val_Icc`, `preimage_subtype_val_Ici`, `preimage_subtype_val_Ico`, `preimage_subtype_val_Iic`, `preimage_subtype_val_Iio`, `preimage_subtype_val_Ioc`, `preimage_subtype_val_Ioi`, `preimage_subtype_val_Ioo`, `image_Ico_subset`, `image_Iio_subset`, `image_Ioc_subset`, `image_Ioi_subset`, `image_Ioo_subset`, `mapsTo_Ico`, `mapsTo_Iio`, `mapsTo_Ioc`, `mapsTo_Ioi`, `mapsTo_Ioo`, `image_Ico_subset`, `image_Iio_subset`, `image_Ioc_subset`, `image_Ioi_subset`, `image_Ioo_subset`, `mapsTo_Ico`, `mapsTo_Iio`, `mapsTo_Ioc`, `mapsTo_Ioi`, `mapsTo_Ioo`, `image_Ico_subset`, `image_Iio_subset`, `image_Ioc_subset`, `image_Ioi_subset`, `image_Ioo_subset`, `mapsTo_Ico`, `mapsTo_Iio`, `mapsTo_Ioc`, `mapsTo_Ioi`, `mapsTo_Ioo`, `image_Ico_subset`, `image_Iio_subset`, `image_Ioc_subset`, `image_Ioi_subset`, `image_Ioo_subset`, `mapsTo_Ico`, `mapsTo_Iio`, `mapsTo_Ioc`, `mapsTo_Ioi`, `mapsTo_Ioo`, `directedOn_ge_Icc`, `directedOn_ge_Ici`, `directedOn_ge_Ico`, `directedOn_le_Icc`, `directedOn_le_Iic`, `directedOn_le_Ioc`	118
Total	118

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Icc_subset` 📖	mathematical	`Antitone`	`Set` `Set.instHasSubset` `Set.image` `Set.Icc`	—	`AntitoneOn.image_Icc_subset` `antitoneOn`
`image_Ici_subset` 📖	mathematical	`Antitone`	`Set` `Set.instHasSubset` `Set.image` `Set.Ici` `Set.Iic`	—	`AntitoneOn.image_Ici_subset` `antitoneOn`
`image_Iic_subset` 📖	mathematical	`Antitone`	`Set` `Set.instHasSubset` `Set.image` `Set.Iic` `Set.Ici`	—	`AntitoneOn.image_Iic_subset` `antitoneOn`
`mapsTo_Icc` 📖	mathematical	`Antitone`	`Set.MapsTo` `Set.Icc`	—	`AntitoneOn.mapsTo_Icc` `antitoneOn`
`mapsTo_Ici` 📖	mathematical	`Antitone`	`Set.MapsTo` `Set.Ici` `Set.Iic`	—	`AntitoneOn.mapsTo_Ici` `antitoneOn`
`mapsTo_Iic` 📖	mathematical	`Antitone`	`Set.MapsTo` `Set.Iic` `Set.Ici`	—	`AntitoneOn.mapsTo_Iic` `antitoneOn`

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Icc_subset` 📖	mathematical	`AntitoneOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.image`	—	`Set.MapsTo.image_subset` `mapsTo_Icc`
`image_Ici_subset` 📖	mathematical	`AntitoneOn` `Set.Ici`	`Set` `Set.instHasSubset` `Set.image` `Set.Iic`	—	`Set.MapsTo.image_subset` `mapsTo_Ici`
`image_Iic_subset` 📖	mathematical	`AntitoneOn` `Set.Iic`	`Set` `Set.instHasSubset` `Set.image` `Set.Ici`	—	`Set.MapsTo.image_subset` `mapsTo_Iic`
`mapsTo_Icc` 📖	mathematical	`AntitoneOn` `Set.Icc`	`Set.MapsTo`	—	`Set.right_mem_Icc` `LE.le.trans` `Set.left_mem_Icc`
`mapsTo_Ici` 📖	mathematical	`AntitoneOn` `Set.Ici`	`Set.MapsTo` `Set.Iic`	—	—
`mapsTo_Iic` 📖	mathematical	`AntitoneOn` `Set.Iic`	`Set.MapsTo` `Set.Ici`	—	—

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Icc_subset` 📖	mathematical	`Monotone`	`Set` `Set.instHasSubset` `Set.image` `Set.Icc`	—	`MonotoneOn.image_Icc_subset` `monotoneOn`
`image_Ici_subset` 📖	mathematical	`Monotone`	`Set` `Set.instHasSubset` `Set.image` `Set.Ici`	—	`MonotoneOn.image_Ici_subset` `monotoneOn`
`image_Iic_subset` 📖	mathematical	`Monotone`	`Set` `Set.instHasSubset` `Set.image` `Set.Iic`	—	`MonotoneOn.image_Iic_subset` `monotoneOn`
`mapsTo_Icc` 📖	mathematical	`Monotone`	`Set.MapsTo` `Set.Icc`	—	`MonotoneOn.mapsTo_Icc` `monotoneOn`
`mapsTo_Ici` 📖	mathematical	`Monotone`	`Set.MapsTo` `Set.Ici`	—	`MonotoneOn.mapsTo_Ici` `monotoneOn`
`mapsTo_Iic` 📖	mathematical	`Monotone`	`Set.MapsTo` `Set.Iic`	—	`MonotoneOn.mapsTo_Iic` `monotoneOn`

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Icc_subset` 📖	mathematical	`MonotoneOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.image`	—	`Set.MapsTo.image_subset` `mapsTo_Icc`
`image_Ici_subset` 📖	mathematical	`MonotoneOn` `Set.Ici`	`Set` `Set.instHasSubset` `Set.image`	—	`Set.MapsTo.image_subset` `mapsTo_Ici`
`image_Iic_subset` 📖	mathematical	`MonotoneOn` `Set.Iic`	`Set` `Set.instHasSubset` `Set.image`	—	`Set.MapsTo.image_subset` `mapsTo_Iic`
`mapsTo_Icc` 📖	mathematical	`MonotoneOn` `Set.Icc`	`Set.MapsTo`	—	`Set.left_mem_Icc` `LE.le.trans` `Set.right_mem_Icc`
`mapsTo_Ici` 📖	mathematical	`MonotoneOn` `Set.Ici`	`Set.MapsTo`	—	—
`mapsTo_Iic` 📖	mathematical	`MonotoneOn` `Set.Iic`	`Set.MapsTo`	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_subtype_val_Icc_Ici` 📖	mathematical	—	`image` `Set` `instMembership` `Icc` `Ici` `Subtype.preorder`	—	`LE.le.trans`
`image_subtype_val_Icc_Iic` 📖	mathematical	—	`image` `Set` `instMembership` `Icc` `Iic` `Subtype.preorder`	—	`le_trans`
`image_subtype_val_Icc_Iio` 📖	mathematical	—	`image` `Set` `instMembership` `Icc` `Iio` `Subtype.preorder` `Ico`	—	`LE.le.trans` `le_of_lt`
`image_subtype_val_Icc_Ioi` 📖	mathematical	—	`image` `Set` `instMembership` `Icc` `Ioi` `Subtype.preorder` `Ioc`	—	`LE.le.trans` `le_of_lt`
`image_subtype_val_Icc_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `Icc` `Subtype.preorder`	—	`image_subset_iff`
`image_subtype_val_Ici_Ici` 📖	mathematical	—	`image` `Set` `instMembership` `Ici` `Subtype.preorder`	—	`Subtype.image_preimage_val` `inter_eq_right` `Ici_subset_Ici`
`image_subtype_val_Ici_Iic` 📖	mathematical	—	`image` `Set` `instMembership` `Ici` `Iic` `Subtype.preorder` `Icc`	—	`Subtype.image_preimage_val` `Ici_inter_Iic`
`image_subtype_val_Ici_Iio` 📖	mathematical	—	`image` `Set` `instMembership` `Ici` `Iio` `Subtype.preorder` `Ico`	—	`Subtype.image_preimage_val` `Ici_inter_Iio`
`image_subtype_val_Ici_Ioi` 📖	mathematical	—	`image` `Set` `instMembership` `Ici` `Ioi` `Subtype.preorder`	—	`Subtype.image_preimage_val` `inter_eq_right` `Ioi_subset_Ici`
`image_subtype_val_Ici_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `Ici` `Subtype.preorder`	—	`image_subset_iff`
`image_subtype_val_Ico_Ici` 📖	mathematical	—	`image` `Set` `instMembership` `Ico` `Ici` `Subtype.preorder`	—	`LE.le.trans`
`image_subtype_val_Ico_Iic` 📖	mathematical	—	`image` `Set` `instMembership` `Ico` `Iic` `Subtype.preorder` `Icc`	—	`lt_of_le_of_lt`
`image_subtype_val_Ico_Iio` 📖	mathematical	—	`image` `Set` `instMembership` `Ico` `Iio` `Subtype.preorder`	—	`lt_trans`
`image_subtype_val_Ico_Ioi` 📖	mathematical	—	`image` `Set` `instMembership` `Ico` `Ioi` `Subtype.preorder` `Ioo`	—	`LE.le.trans` `le_of_lt`
`image_subtype_val_Ico_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `Ico` `Subtype.preorder`	—	`image_subset_iff`
`image_subtype_val_Iic_Ici` 📖	mathematical	—	`image` `Set` `instMembership` `Iic` `Ici` `Subtype.preorder` `Icc`	—	`Subtype.image_preimage_val` `inter_comm`
`image_subtype_val_Iic_Iic` 📖	mathematical	—	`image` `Set` `instMembership` `Iic` `Subtype.preorder`	—	`image_subtype_val_Ici_Ici`
`image_subtype_val_Iic_Iio` 📖	mathematical	—	`image` `Set` `instMembership` `Iic` `Iio` `Subtype.preorder`	—	`image_subtype_val_Ici_Ioi`
`image_subtype_val_Iic_Ioi` 📖	mathematical	—	`image` `Set` `instMembership` `Iic` `Ioi` `Subtype.preorder` `Ioc`	—	`Subtype.image_preimage_val` `inter_comm`
`image_subtype_val_Iic_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `Iic` `Subtype.preorder`	—	`image_subset_iff`
`image_subtype_val_Iio_Ici` 📖	mathematical	—	`image` `Set` `instMembership` `Iio` `Ici` `Subtype.preorder` `Ico`	—	`Subtype.image_preimage_val` `inter_comm`
`image_subtype_val_Iio_Iic` 📖	mathematical	—	`image` `Set` `instMembership` `Iio` `Iic` `Subtype.preorder`	—	`image_subtype_val_Ioi_Ici`
`image_subtype_val_Iio_Iio` 📖	mathematical	—	`image` `Set` `instMembership` `Iio` `Subtype.preorder`	—	`image_subtype_val_Ioi_Ioi`
`image_subtype_val_Iio_Ioi` 📖	mathematical	—	`image` `Set` `instMembership` `Iio` `Ioi` `Subtype.preorder` `Ioo`	—	`Subtype.image_preimage_val` `inter_comm`
`image_subtype_val_Iio_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `Iio` `Subtype.preorder`	—	`image_subset_iff`
`image_subtype_val_Ioc_Ici` 📖	mathematical	—	`image` `Set` `instMembership` `Ioc` `Ici` `Subtype.preorder` `Icc`	—	`LT.lt.trans_le`
`image_subtype_val_Ioc_Iic` 📖	mathematical	—	`image` `Set` `instMembership` `Ioc` `Iic` `Subtype.preorder`	—	`le_trans`
`image_subtype_val_Ioc_Iio` 📖	mathematical	—	`image` `Set` `instMembership` `Ioc` `Iio` `Subtype.preorder` `Ioo`	—	`LE.le.trans` `le_of_lt`
`image_subtype_val_Ioc_Ioi` 📖	mathematical	—	`image` `Set` `instMembership` `Ioc` `Ioi` `Subtype.preorder`	—	`LT.lt.trans`
`image_subtype_val_Ioc_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `Ioc` `Subtype.preorder`	—	`image_subset_iff`
`image_subtype_val_Ioi_Ici` 📖	mathematical	—	`image` `Set` `instMembership` `Ioi` `Ici` `Subtype.preorder`	—	`Subtype.image_preimage_val` `inter_eq_right` `Ici_subset_Ioi`
`image_subtype_val_Ioi_Iic` 📖	mathematical	—	`image` `Set` `instMembership` `Ioi` `Iic` `Subtype.preorder` `Ioc`	—	`Subtype.image_preimage_val` `Ioi_inter_Iic`
`image_subtype_val_Ioi_Iio` 📖	mathematical	—	`image` `Set` `instMembership` `Ioi` `Iio` `Subtype.preorder` `Ioo`	—	`Subtype.image_preimage_val` `Ioi_inter_Iio`
`image_subtype_val_Ioi_Ioi` 📖	mathematical	—	`image` `Set` `instMembership` `Ioi` `Subtype.preorder`	—	`Subtype.image_preimage_val` `inter_eq_right` `Ioi_subset_Ioi` `LT.lt.le`
`image_subtype_val_Ioi_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `Ioi` `Subtype.preorder`	—	`image_subset_iff`
`image_subtype_val_Ioo_Ici` 📖	mathematical	—	`image` `Set` `instMembership` `Ioo` `Ici` `Subtype.preorder` `Ico`	—	`LT.lt.trans_le`
`image_subtype_val_Ioo_Iic` 📖	mathematical	—	`image` `Set` `instMembership` `Ioo` `Iic` `Subtype.preorder` `Ioc`	—	`lt_of_le_of_lt`
`image_subtype_val_Ioo_Iio` 📖	mathematical	—	`image` `Set` `instMembership` `Ioo` `Iio` `Subtype.preorder`	—	`lt_trans`
`image_subtype_val_Ioo_Ioi` 📖	mathematical	—	`image` `Set` `instMembership` `Ioo` `Ioi` `Subtype.preorder`	—	`LT.lt.trans`
`image_subtype_val_Ioo_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `Ioo` `Subtype.preorder`	—	`image_subset_iff`
`preimage_subtype_val_Icc` 📖	mathematical	—	`preimage` `Icc` `Subtype.preorder`	—	—
`preimage_subtype_val_Ici` 📖	mathematical	—	`preimage` `Ici` `Subtype.preorder`	—	—
`preimage_subtype_val_Ico` 📖	mathematical	—	`preimage` `Ico` `Subtype.preorder`	—	—
`preimage_subtype_val_Iic` 📖	mathematical	—	`preimage` `Iic` `Subtype.preorder`	—	—
`preimage_subtype_val_Iio` 📖	mathematical	—	`preimage` `Iio` `Subtype.preorder`	—	—
`preimage_subtype_val_Ioc` 📖	mathematical	—	`preimage` `Ioc` `Subtype.preorder`	—	—
`preimage_subtype_val_Ioi` 📖	mathematical	—	`preimage` `Ioi` `Subtype.preorder`	—	—
`preimage_subtype_val_Ioo` 📖	mathematical	—	`preimage` `Ioo` `Subtype.preorder`	—	—

StrictAnti

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Ico_subset` 📖	mathematical	`StrictAnti` `PartialOrder.toPreorder`	`Set` `Set.instHasSubset` `Set.image` `Set.Ico` `Set.Ioc`	—	`StrictAntiOn.image_Ico_subset` `strictAntiOn`
`image_Iio_subset` 📖	mathematical	`StrictAnti`	`Set` `Set.instHasSubset` `Set.image` `Set.Iio` `Set.Ioi`	—	`StrictAntiOn.image_Iio_subset` `strictAntiOn`
`image_Ioc_subset` 📖	mathematical	`StrictAnti` `PartialOrder.toPreorder`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioc` `Set.Ico`	—	`StrictAntiOn.image_Ioc_subset` `strictAntiOn`
`image_Ioi_subset` 📖	mathematical	`StrictAnti`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioi` `Set.Iio`	—	`StrictAntiOn.image_Ioi_subset` `strictAntiOn`
`image_Ioo_subset` 📖	mathematical	`StrictAnti`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioo`	—	`StrictAntiOn.image_Ioo_subset` `strictAntiOn`
`mapsTo_Ico` 📖	mathematical	`StrictAnti` `PartialOrder.toPreorder`	`Set.MapsTo` `Set.Ico` `Set.Ioc`	—	`StrictAntiOn.mapsTo_Ico` `strictAntiOn`
`mapsTo_Iio` 📖	mathematical	`StrictAnti`	`Set.MapsTo` `Set.Iio` `Set.Ioi`	—	`StrictAntiOn.mapsTo_Iio` `strictAntiOn`
`mapsTo_Ioc` 📖	mathematical	`StrictAnti` `PartialOrder.toPreorder`	`Set.MapsTo` `Set.Ioc` `Set.Ico`	—	`StrictAntiOn.mapsTo_Ioc` `strictAntiOn`
`mapsTo_Ioi` 📖	mathematical	`StrictAnti`	`Set.MapsTo` `Set.Ioi` `Set.Iio`	—	`StrictAntiOn.mapsTo_Ioi` `strictAntiOn`
`mapsTo_Ioo` 📖	mathematical	`StrictAnti`	`Set.MapsTo` `Set.Ioo`	—	`StrictAntiOn.mapsTo_Ioo` `strictAntiOn`

StrictAntiOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Ico_subset` 📖	mathematical	`StrictAntiOn` `PartialOrder.toPreorder` `Set.Icc`	`Set` `Set.instHasSubset` `Set.image` `Set.Ico` `Set.Ioc`	—	`Set.MapsTo.image_subset` `mapsTo_Ico`
`image_Iio_subset` 📖	mathematical	`StrictAntiOn` `Set.Iic`	`Set` `Set.instHasSubset` `Set.image` `Set.Iio` `Set.Ioi`	—	`Set.MapsTo.image_subset` `mapsTo_Iio`
`image_Ioc_subset` 📖	mathematical	`StrictAntiOn` `PartialOrder.toPreorder` `Set.Icc`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioc` `Set.Ico`	—	`Set.MapsTo.image_subset` `mapsTo_Ioc`
`image_Ioi_subset` 📖	mathematical	`StrictAntiOn` `Set.Ici`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioi` `Set.Iio`	—	`Set.MapsTo.image_subset` `mapsTo_Ioi`
`image_Ioo_subset` 📖	mathematical	`StrictAntiOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioo`	—	`Set.MapsTo.image_subset` `mapsTo_Ioo`
`mapsTo_Ico` 📖	mathematical	`StrictAntiOn` `PartialOrder.toPreorder` `Set.Icc`	`Set.MapsTo` `Set.Ico` `Set.Ioc`	—	`Set.Ico_subset_Icc_self` `Set.right_mem_Icc` `LE.le.trans` `LT.lt.le` `antitoneOn` `Set.left_mem_Icc`
`mapsTo_Iio` 📖	mathematical	`StrictAntiOn` `Set.Iic`	`Set.MapsTo` `Set.Iio` `Set.Ioi`	—	`LT.lt.le` `le_rfl`
`mapsTo_Ioc` 📖	mathematical	`StrictAntiOn` `PartialOrder.toPreorder` `Set.Icc`	`Set.MapsTo` `Set.Ioc` `Set.Ico`	—	`antitoneOn` `Set.Ioc_subset_Icc_self` `Set.right_mem_Icc` `LE.le.trans` `LT.lt.le` `Set.left_mem_Icc`
`mapsTo_Ioi` 📖	mathematical	`StrictAntiOn` `Set.Ici`	`Set.MapsTo` `Set.Ioi` `Set.Iio`	—	`le_rfl` `LT.lt.le`
`mapsTo_Ioo` 📖	mathematical	`StrictAntiOn` `Set.Icc`	`Set.MapsTo` `Set.Ioo`	—	`Set.Ioo_subset_Icc_self` `Set.right_mem_Icc` `LT.lt.le` `LT.lt.trans` `Set.left_mem_Icc`

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Ico_subset` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder`	`Set` `Set.instHasSubset` `Set.image` `Set.Ico`	—	`StrictMonoOn.image_Ico_subset` `strictMonoOn`
`image_Iio_subset` 📖	mathematical	`StrictMono`	`Set` `Set.instHasSubset` `Set.image` `Set.Iio`	—	`StrictMonoOn.image_Iio_subset` `strictMonoOn`
`image_Ioc_subset` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioc`	—	`StrictMonoOn.image_Ioc_subset` `strictMonoOn`
`image_Ioi_subset` 📖	mathematical	`StrictMono`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioi`	—	`StrictMonoOn.image_Ioi_subset` `strictMonoOn`
`image_Ioo_subset` 📖	mathematical	`StrictMono`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioo`	—	`StrictMonoOn.image_Ioo_subset` `strictMonoOn`
`mapsTo_Ico` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder`	`Set.MapsTo` `Set.Ico`	—	`StrictMonoOn.mapsTo_Ico` `strictMonoOn`
`mapsTo_Iio` 📖	mathematical	`StrictMono`	`Set.MapsTo` `Set.Iio`	—	`StrictMonoOn.mapsTo_Iio` `strictMonoOn`
`mapsTo_Ioc` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder`	`Set.MapsTo` `Set.Ioc`	—	`StrictMonoOn.mapsTo_Ioc` `strictMonoOn`
`mapsTo_Ioi` 📖	mathematical	`StrictMono`	`Set.MapsTo` `Set.Ioi`	—	`StrictMonoOn.mapsTo_Ioi` `strictMonoOn`
`mapsTo_Ioo` 📖	mathematical	`StrictMono`	`Set.MapsTo` `Set.Ioo`	—	`StrictMonoOn.mapsTo_Ioo` `strictMonoOn`

StrictMonoOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Ico_subset` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `Set.Icc`	`Set` `Set.instHasSubset` `Set.image` `Set.Ico`	—	`Set.MapsTo.image_subset` `mapsTo_Ico`
`image_Iio_subset` 📖	mathematical	`StrictMonoOn` `Set.Iic`	`Set` `Set.instHasSubset` `Set.image` `Set.Iio`	—	`Set.MapsTo.image_subset` `mapsTo_Iio`
`image_Ioc_subset` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `Set.Icc`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioc`	—	`Set.MapsTo.image_subset` `mapsTo_Ioc`
`image_Ioi_subset` 📖	mathematical	`StrictMonoOn` `Set.Ici`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioi`	—	`Set.MapsTo.image_subset` `mapsTo_Ioi`
`image_Ioo_subset` 📖	mathematical	`StrictMonoOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.image` `Set.Ioo`	—	`Set.MapsTo.image_subset` `mapsTo_Ioo`
`mapsTo_Ico` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `Set.Icc`	`Set.MapsTo` `Set.Ico`	—	`monotoneOn` `Set.left_mem_Icc` `LE.le.trans` `LT.lt.le` `Set.Ico_subset_Icc_self` `Set.right_mem_Icc`
`mapsTo_Iio` 📖	mathematical	`StrictMonoOn` `Set.Iic`	`Set.MapsTo` `Set.Iio`	—	`LT.lt.le` `le_rfl`
`mapsTo_Ioc` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `Set.Icc`	`Set.MapsTo` `Set.Ioc`	—	`Set.left_mem_Icc` `LE.le.trans` `LT.lt.le` `Set.Ioc_subset_Icc_self` `monotoneOn` `Set.right_mem_Icc`
`mapsTo_Ioi` 📖	mathematical	`StrictMonoOn` `Set.Ici`	`Set.MapsTo` `Set.Ioi`	—	`le_rfl` `LT.lt.le`
`mapsTo_Ioo` 📖	mathematical	`StrictMonoOn` `Set.Icc`	`Set.MapsTo` `Set.Ioo`	—	`Set.left_mem_Icc` `LT.lt.le` `LT.lt.trans` `Set.Ioo_subset_Icc_self` `Set.right_mem_Icc`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directedOn_ge_Icc` 📖	mathematical	—	`DirectedOn` `Preorder.toLE` `Set.Icc`	—	`Set.left_mem_Icc` `LE.le.trans`
`directedOn_ge_Ici` 📖	mathematical	—	`DirectedOn` `Preorder.toLE` `Set.Ici`	—	`le_rfl`
`directedOn_ge_Ico` 📖	mathematical	—	`DirectedOn` `Preorder.toLE` `Set.Ico`	—	`Set.left_mem_Ico` `LE.le.trans_lt`
`directedOn_le_Icc` 📖	mathematical	—	`DirectedOn` `Preorder.toLE` `Set.Icc`	—	`Set.right_mem_Icc` `LE.le.trans`
`directedOn_le_Iic` 📖	mathematical	—	`DirectedOn` `Preorder.toLE` `Set.Iic`	—	`le_rfl`
`directedOn_le_Ioc` 📖	mathematical	—	`DirectedOn` `Preorder.toLE` `Set.Ioc`	—	`Set.right_mem_Ioc` `LT.lt.trans_le`

---

← Back to Index