Theorem LowerSet.Iic_strictMono

Modification history

2026-03-21 16:01
Mathlib/Order/UpperLower/Principal.lean
chore(Order/UpperLower/Principal): use `to_dual` (#36945) …
Deleted LowerSet.Iic_strictMonoView on Github →
2025-07-05 03:31
Mathlib/Order/UpperLower/Principal.lean
feat(Order): StrictMono of UpperSet/LowerSet.Iic/Iio/Ici/Ioi (#26756)
Added LowerSet.Iic_strictMonoView on Github →