Commit 2023-01-23 08:16 7aa98b6c

View on Github →

feat : port Algebra.Star.Pointwise (#1749)

Estimated changes

added theorem Set.Finite.star
added theorem Set.Nonempty.star
added theorem Set.compl_star
added theorem Set.image_star
added theorem Set.inter_star
added theorem Set.interᵢ_star
added theorem Set.mem_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
added theorem Set.unionᵢ_star
modified theorem Set.image2_mul