Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-26 16:53 3b49fe25

View on Github →

feat(algebra/star/pointwise, algebra/star/basic): add pointwise star, and a few convenience lemmas (#12290) This adds a star operation to sets in the pointwise locale and establishes the basic properties. The names and proofs were taken from the corresponding ones for inv. A few extras were added.

Estimated changes

added theorem eq_star_iff_eq_star
added theorem eq_star_of_eq_star
added theorem star_eq_iff_star_eq
added theorem set.Inter_star
added theorem set.Union_star
added theorem set.compl_star
added theorem set.finite.star
added theorem set.image_star
added theorem set.inter_star
added theorem set.mem_star
added theorem set.nonempty.star
added theorem set.nonempty_star
added theorem set.star_empty
added theorem set.star_mem_star
added theorem set.star_preimage
added theorem set.star_singleton
added theorem set.star_subset
added theorem set.star_subset_star
added theorem set.star_univ
added theorem set.union_star