Commit 2023-12-10 10:44 f13f1972

View on Github →

chore: Rename Set.Sigma to Set.sigma (#8927) This was a misport. Also adds missing whitespace after some Σs while we're here, and some other arbitrary lime re-wrappings.

Estimated changes

modified theorem Set.Nonempty.sigma_fst
modified theorem Set.Nonempty.sigma_snd
modified theorem Set.empty_sigma
modified theorem Set.forall_sigma_iff
modified theorem Set.fst_image_sigma
modified theorem Set.fst_image_sigma_subset
modified theorem Set.insert_sigma
modified theorem Set.mem_sigma_iff
modified theorem Set.mk_mem_sigma
modified theorem Set.mk_preimage_sigma
modified theorem Set.mk_sigma_iff
modified theorem Set.sigma_diff_sigma
modified theorem Set.sigma_empty
modified theorem Set.sigma_eq_empty_iff
modified theorem Set.sigma_inter_sigma
modified theorem Set.sigma_mono
modified theorem Set.sigma_nonempty_iff
modified theorem Set.sigma_subset_iff
modified theorem Set.sigma_union
modified theorem Set.sigma_univ
modified theorem Set.singleton_sigma
modified theorem Set.union_sigma
modified theorem Set.univ_sigma_univ