Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-08 07:36 ac6fc38e

View on Github →

chore(*): move/add lemmas about disjoint (#5277)

  • set.disjoint_compl_left and set.disjoint_compl_right:
    • generalize to any boolean_algebra,
    • move to order/boolean_algebra,
    • drop set. prefix,
    • make the argument implicit to follow the style of other lemmas in order/boolean_algebra
  • add set.disjoint_empty and set.empty_disjoint
  • add disjoint_top and top_disjoint, use in set.disjoint_univand set.univ_disjoint.

Estimated changes

deleted theorem set.disjoint_compl_left
deleted theorem set.disjoint_compl_right
added theorem set.disjoint_empty
added theorem set.empty_disjoint
added theorem disjoint_compl_left
added theorem disjoint_compl_right
modified theorem disjoint_bot_left
modified theorem disjoint_bot_right
added theorem disjoint_top
added theorem top_disjoint