Theorem Set.image_subtype_val_Iio_Iic

Modification history

2026-09-08 16:08

Mathlib/Order/Interval/Set/Image.lean

chore(Order/Interval/Set/Image): use `to_dual` (#43584)

Deleted Set.image_subtype_val_Iio_Iic View on Github →

2023-10-30 08:37

Mathlib/Data/Set/Intervals/Image.lean

feat(Data/Set): images of intervals under `Subtype.val` (#7653) …

Added Set.image_subtype_val_Iio_Iic View on Github →