Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-20 20:07 4b9d94dc

View on Github →

feat(data/[fin]set): add some more basic properties of (finite) sets (#948)

  • feat(data/[fin]set): add some more basic properties of (finite) sets
  • update after reviews
  • fix error, move pairwise_disjoint to lattice as well
  • fix error

Estimated changes

added theorem finset.to_set_sdiff
added theorem set.compl_empty_iff
added theorem set.compl_univ_iff
added theorem set.image_congr'
added theorem set.image_eq_range
added theorem set.image_id'
added theorem set.image_image
added theorem set.mem_diff_singleton
added theorem set.nonempty_compl
added theorem set.nonempty_image
added theorem set.subset_insert_diff
added theorem subtype.range_val
added theorem set.finite_bUnion'
added theorem set.inj_on_preimage
added theorem disjoint_self
added theorem ne_of_disjoint
added theorem set.Union_of_singleton