Mathlib v3 is deprecated. Go to Mathlib v4

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 with compl_compl';
  • add is_compl.compl_eq_iff, compl_eq_top, and compl_eq_bot;
  • add simp attribute to compl_le_compl_iff_le;
  • fix misleading name in compl_le_iff_compl_le, add a missing variant;
  • add simp attribute to compl_empty_iff and compl_univ_iff;
  • add set.subset.eventually_le.

Estimated changes

deleted theorem set.compl_compl
modified theorem set.compl_empty
modified theorem set.compl_empty_iff
modified theorem set.compl_inter
modified theorem set.compl_inter_self
modified theorem set.compl_union
modified theorem set.compl_univ
modified theorem set.compl_univ_iff
modified theorem set.inter_compl_self
deleted theorem compl_compl'
added theorem compl_compl
added theorem compl_eq_bot
added theorem compl_eq_top
modified theorem compl_le_compl_iff_le
modified theorem compl_le_iff_compl_le
added theorem is_compl.compl_eq_iff
added theorem le_compl_iff_le_compl