Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subsingleton_of_top_le_bot

Modification history

2021-11-23 13:11
src/order/bounded_order.lean
refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891) …
Modified subsingleton_of_top_le_botView on Github →
2020-10-17 18:25
src/order/bounded_lattice.lean
feat(algebra/algebra/subalgebra): subalgebra.subsingleton (#4631)
Added subsingleton_of_top_le_botView on Github →