Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-28 19:09 7db76670

View on Github →

feat(order/boolean_algebra): Interaction of disjointness and complements (#14925) Prove disjoint x yᶜ ↔ x ≤ y and similar, transfer those results to set. Lemma renames

  • subset_compl_iff_disjointsubset_compl_iff_disjoint_right
  • set.subset_compl_iff_disjointset.subset_compl_iff_disjoint_right
  • disjoint_iff_le_compl_leftle_compl_iff_disjoint_left
  • disjoint_iff_le_compl_rightle_compl_iff_disjoint_right

Estimated changes