Commit 2021-08-01 09:36 5b9b4557
View on Github →chore(order/complete_lattice): generalize Sup_eq_supr'
, add lemmas (#8484)
Sup_eq_supr'
only needs[has_Sup α]
, addInf_eq_infi'
;- add
supr_range'
,infi_range'
,Sup_image'
,Inf_image'
lemmas that use supremum/infimum over subtypes and only require[has_Sup]
/[has_Inf]
.