Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-22 09:49 5bff97f2

View on Github →

chore(data/set/basic): reflow/golf some proofs (#17066)

  • reuse facts about order_top;
  • use alias;
  • add set.ssubset_univ_iff;
  • replace some proofs with iff.rfl/rfl.

Estimated changes

modified theorem set.compl_ne_eq_singleton
modified theorem set.compl_singleton_eq
modified theorem set.mem_compl_singleton_iff
modified theorem set.nonempty_compl
added theorem set.ssubset_univ_iff
modified theorem set.univ_subset_iff