Theorem UpperSet.Ici_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 UpperSet.Ici_strictMonoView on Github →