Commit 2021-01-14 15:25 82532c19
View on Github →chore(data/set/basic): reuse some proofs about boolean_algebra
(#5728)
API changes:
- merge
set.compl_compl
withcompl_compl'
; - add
is_compl.compl_eq_iff
,compl_eq_top
, andcompl_eq_bot
; - add
simp
attribute tocompl_le_compl_iff_le
; - fix misleading name in
compl_le_iff_compl_le
, add a missing variant; - add
simp
attribute tocompl_empty_iff
andcompl_univ_iff
; - add
set.subset.eventually_le
.