Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq_singleton_bot_of_Sup_eq_bot_of_nonempty

Modification history

2021-01-04 05:36

src/order/complete_lattice.lean

feat(data/*, order/*) supporting lemmas for characterising well-founded complete lattices (#5446)

Added eq_singleton_bot_of_Sup_eq_bot_of_nonempty View on Github →