Theorem LowerSet.Iio_eq_bot

Modification history

2026-03-21 16:01
Mathlib/Order/UpperLower/Principal.lean
chore(Order/UpperLower/Principal): use `to_dual` (#36945) …
Deleted LowerSet.Iio_eq_botView on Github →
2025-08-14 21:19
Mathlib/Order/UpperLower/Principal.lean
feat(Algebra/Order): ArchimedeanClass ball (#27885) …
Added LowerSet.Iio_eq_botView on Github →