Commit 2020-04-26 03:56 bda206ab

View on Github →

chore(data/option,order/bounded_lattice): 2 simple lemmas about get_or_else (#2531) I'm going to use these lemmas for polynomial.nat_degree. I don't want to PR this change to data/polynomial because this would create merge conflicts later.

Estimated changes

Modified src/data/option/basic.lean

added theorem option.get_or_else_of_ne_none

Modified src/order/bounded_lattice.lean

modified theorem with_bot.bot_lt_coe

modified theorem with_bot.bot_lt_some

added theorem with_bot.le_coe_get_or_else