Commit 2024-01-18 02:11 9fb36425

View on Github →

chore(Data/Set): move definitions to a new file (#9737) This and other similar PRs will help us reduce import dependencies and improve parallel compilation in the future.

Estimated changes

deleted def Set.Elem
deleted theorem Set.diff_eq
deleted theorem Set.mem_compl_iff
deleted theorem Set.mem_diff
deleted theorem Set.mem_diff_of_mem
deleted theorem Set.mem_setOf_eq
deleted theorem Set.mem_univ
added def Set.BijOn
added def Set.Elem
added def Set.EqOn
added def Set.InjOn
added def Set.InvOn
added def Set.LeftInvOn
added def Set.MapsTo
added def Set.RightInvOn
added def Set.SurjOn
added def Set.diagonal
added theorem Set.diff_eq
added def Set.graphOn
added def Set.image2
added def Set.kernImage
added theorem Set.mapsTo_image
added theorem Set.mapsTo_preimage
added theorem Set.mem_compl_iff
added theorem Set.mem_diagonal
added theorem Set.mem_diagonal_iff
added theorem Set.mem_diff
added theorem Set.mem_diff_of_mem
added theorem Set.mem_image2
added theorem Set.mem_image2_of_mem
added theorem Set.mem_image
added theorem Set.mem_image_of_mem
added theorem Set.mem_offDiag
added theorem Set.mem_pi
added theorem Set.mem_preimage
added theorem Set.mem_prod
added theorem Set.mem_prod_eq
added theorem Set.mem_range
added theorem Set.mem_range_self
added theorem Set.mem_seq_iff
added theorem Set.mem_setOf_eq
added theorem Set.mem_univ
added theorem Set.mem_univ_pi
added theorem Set.mk_mem_prod
added def Set.offDiag
added def Set.pi
added def Set.preimage
added def Set.prod
added theorem Set.prod_eq
added def Set.range
added def Set.seq
added theorem Set.seq_eq_image2
deleted def Set.BijOn
deleted def Set.EqOn
deleted def Set.InjOn
deleted def Set.InvOn
deleted def Set.LeftInvOn
deleted def Set.MapsTo.restrict
deleted def Set.MapsTo
deleted def Set.RightInvOn
deleted def Set.SurjOn
deleted def Set.graphOn
deleted theorem Set.mapsTo_image
deleted theorem Set.mapsTo_preimage
deleted theorem Set.apply_rangeSplitting
deleted theorem Set.comp_rangeSplitting
deleted theorem Set.mem_image
deleted theorem Set.mem_image_of_mem
deleted theorem Set.mem_preimage
deleted theorem Set.mem_range
deleted theorem Set.mem_range_self
deleted def Set.preimage
deleted def Set.range
deleted def Set.kernImage
deleted theorem Set.mem_seq_iff
deleted def Set.seq
deleted theorem Set.seq_eq_image2
deleted theorem Set.subset_kernImage_iff
deleted def Set.image2
deleted theorem Set.mem_image2
deleted theorem Set.mem_image2_of_mem
deleted def Set.diagonal
deleted theorem Set.mem_diagonal
deleted theorem Set.mem_diagonal_iff
deleted theorem Set.mem_offDiag
deleted theorem Set.mem_pi
deleted theorem Set.mem_prod
deleted theorem Set.mem_prod_eq
deleted theorem Set.mem_univ_pi
deleted theorem Set.mk_mem_prod
deleted def Set.offDiag
deleted def Set.pi
deleted def Set.prod
deleted theorem Set.prod_eq