Theorem LowerSet.Iio_strictMono

Modification history

2025-07-05 03:31
Mathlib/Order/UpperLower/Principal.lean
feat(Order): StrictMono of UpperSet/LowerSet.Iic/Iio/Ici/Ioi (#26756)
Added LowerSet.Iio_strictMonoView on Github →