Commit 2022-08-11 13:51 8086825f

View on Github →

chore(order/conditionally_complete_lattice): with_top.coe_infi and with_top.coe_supr (#15975) This adds infi and supr versions of the existing Inf and Sup lemmas, and adds some more general primed lemmas that work when much weaker assumptions are available on α.

Estimated changes

Modified src/order/conditionally_complete_lattice.lean

added theorem with_bot.coe_Inf'

added theorem with_bot.coe_Sup'

added theorem with_bot.coe_infi

added theorem with_bot.coe_supr

added theorem with_bot.csupr_empty

added theorem with_top.cinfi_empty

added theorem with_top.coe_Inf'

modified theorem with_top.coe_Inf

added theorem with_top.coe_Sup'

modified theorem with_top.coe_Sup

added theorem with_top.coe_infi

added theorem with_top.coe_supr