Commit 2021-10-03 20:33 c1936c1f

View on Github →

feat(order/basic): define is_top and is_bot (#9493) These predicates allow us to formulate & prove some theorems simultaneously for the cases [order_top α] and [no_top_order α].

Estimated changes

Modified src/data/set/basic.lean

added theorem set.set_of_eq_eq_singleton'

modified theorem set.set_of_eq_eq_singleton

added theorem set.subsingleton_is_bot

added theorem set.subsingleton_is_top

Modified src/data/set/countable.lean

added theorem set.countable_is_bot

added theorem set.countable_is_top

added theorem set.subsingleton.countable

Modified src/data/set/finite.lean

added theorem set.finite_is_bot

added theorem set.finite_is_top

Modified src/order/basic.lean

added theorem is_bot.unique

added def is_bot

added theorem is_top.unique

added def is_top

added theorem not_is_bot

added theorem not_is_top

Modified src/order/bounded_lattice.lean

added theorem is_bot_iff_eq_bot

added theorem is_top_iff_eq_top