Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-14 11:55 ba76bf75

View on Github →

chore(data/option,data/set): a few lemmas, golf (#8636)

  • add option.subsingleton_iff_is_empty and an instance option.unique;
  • add set.is_compl_range_some_none, set.compl_range_some, set.range_some_inter_none, set.range_some_union_none;
  • split the proof of set.pairwise_on_eq_iff_exists_eq into set.nonempty.pairwise_on_eq_iff_exists_eq and set.pairwise_on_eq_iff_exists_eq. Inspired by #8579

Estimated changes

added theorem set.compl_range_some