Commit 2026-07-17 09:57 d99d52c3

View on Github →

chore(Data): rename setOf to Set.ofPred (#41507) This is in prevision of making Set a one-field structure. ofPred will then be the constructor. Generated by Claude Opus then reviewed line-by-line by myself. Assisted-by: Claude Opus 4.8

Estimated changes

added theorem Set.inv_ofPred
deleted theorem Set.inv_setOf
modified theorem Complex.mem_slitPlane_iff
modified theorem Complex.slitPlane_eq_union
deleted theorem Convex.setOf_const_imp
deleted theorem Convex.setOf_gauge_le
added theorem setOfPred_gauge_le_eq
added theorem setOfPred_gauge_lt_eq'
added theorem setOfPred_gauge_lt_eq
deleted theorem setOf_gauge_le_eq
deleted theorem setOf_gauge_lt_eq'
deleted theorem setOf_gauge_lt_eq
deleted theorem isConnected_setOf_sameRay
deleted theorem isOpen_setOf_nat_le_rank
deleted theorem Matroid.setOf_dep_eq
deleted theorem Matroid.setOf_indep_eq
modified theorem Matroid.isCircuit_antichain
added theorem Finset.setOfPred_mem
deleted theorem Finset.setOf_mem
added theorem Set.toFinset_ofPred
deleted theorem Set.toFinset_setOf
deleted theorem List.set_of_mem_cons
deleted theorem List.setOf_mem_sym2
deleted theorem Multiset.setOf_mem_sym2
modified theorem Nat.count_le_card
modified theorem Nat.count_lt_card
modified theorem Nat.count_le_iff_le_nth
modified theorem Nat.count_nth
modified theorem Nat.count_nth_of_infinite
modified theorem Nat.count_nth_succ
modified theorem Nat.gc_count_nth
modified theorem Nat.image_nth_Iio_card
modified theorem Nat.isLeast_nth
modified theorem Nat.isLeast_nth_of_infinite
modified theorem Nat.isLeast_nth_of_lt_card
modified theorem Nat.le_nth
modified theorem Nat.le_nth_count
modified theorem Nat.lt_nth_iff_count_lt
modified theorem Nat.nth_eq_getD_sort
modified theorem Nat.nth_eq_orderEmbOfFin
modified theorem Nat.nth_eq_orderIsoOfNat
modified theorem Nat.nth_injOn
modified theorem Nat.nth_injective
modified theorem Nat.nth_le_nth'
modified theorem Nat.nth_le_nth
modified theorem Nat.nth_le_nth_of_lt_card
modified theorem Nat.nth_lt_nth'
modified theorem Nat.nth_lt_nth
modified theorem Nat.nth_lt_nth_of_lt_card
modified theorem Nat.nth_mem
modified theorem Nat.nth_mem_of_infinite
modified theorem Nat.nth_mem_of_lt_card
modified theorem Nat.nth_monotone
modified theorem Nat.nth_of_card_le
modified theorem Nat.nth_strictMono
modified theorem Nat.nth_strictMonoOn
modified theorem Nat.nth_zero
modified theorem Nat.range_nth_of_finite
modified theorem Nat.range_nth_of_infinite
modified theorem Nat.range_nth_subset
modified theorem Nat.subset_range_nth
deleted theorem Nat.infinite_setOf_prime
added theorem Set.coe_ofPred
deleted theorem Set.coe_setOf
deleted theorem Set.inter_setOf_eq_sep
added theorem Set.ofPred_and
added theorem Set.ofPred_bijective
added theorem Set.ofPred_bot
added theorem Set.ofPred_false
added theorem Set.ofPred_inj
added theorem Set.ofPred_injective
added theorem Set.ofPred_or
added theorem Set.ofPred_subset
added theorem Set.ofPred_top
added theorem Set.ofPred_true
added theorem Set.sep_ofPred
deleted theorem Set.sep_setOf
added theorem Set.sep_subset_ofPred
deleted theorem Set.sep_subset_setOf
deleted theorem Set.setOf_and
deleted theorem Set.setOf_bijective
deleted theorem Set.setOf_bot
deleted theorem Set.setOf_false
deleted theorem Set.setOf_inj
deleted theorem Set.setOf_injective
deleted theorem Set.setOf_inter_eq_sep
deleted theorem Set.setOf_or
deleted theorem Set.setOf_subset
deleted theorem Set.setOf_subset_setOf
deleted theorem Set.setOf_top
deleted theorem Set.setOf_true
added theorem Set.subset_ofPred
deleted theorem Set.subset_setOf
added def Set.ofPred
deleted def setOf
added theorem Set.compl_image_ofPred
deleted theorem Set.compl_image_set_of
added theorem Set.preimage_ofPred_eq
deleted theorem Set.preimage_setOf_eq
deleted theorem Set.setOf_eq_eq_singleton
added theorem Set.iInter_ofPred
deleted theorem Set.iInter_setOf
added theorem Set.iUnion_ofPred
deleted theorem Set.iUnion_setOf
added theorem Set.ofPred_exists
added theorem Set.ofPred_forall
deleted theorem Set.setOf_exists
deleted theorem Set.setOf_forall
added theorem Set.eq_mem_ofPred
deleted theorem Set.eq_mem_setOf
added theorem Set.mem_ofPred
added theorem Set.mem_ofPred_eq
deleted theorem Set.mem_setOf
deleted theorem Set.mem_setOf_eq
added theorem Set.notMem_ofPred_iff
deleted theorem Set.notMem_setOf_iff
added theorem Set.ofPred_mem_eq
deleted theorem Set.setOf_mem_eq
added theorem Set.antitone_ofPred
deleted theorem Set.antitone_setOf
added theorem Set.monotone_ofPred
deleted theorem Set.monotone_setOf
deleted theorem SetLike.setOf_mem_eq
modified theorem IndexedPartition.class_of
deleted theorem measurableSet_setOf
modified theorem measurable_mem
deleted theorem measurable_setOf
added theorem measurable_setOfPred
deleted theorem MeasurableEquiv.coe_setOf
deleted theorem Set.DefinableFun.setOf_eq
deleted theorem volume_setOf_liouville
deleted theorem IsGδ.setOf_liouville
deleted theorem setOf_maximal_antichain
deleted theorem setOf_minimal_antichain
added theorem Set.compl_ofPred
deleted theorem Set.compl_setOf
deleted theorem isCofinal_setOf_imp_lt
modified def maxChain
deleted theorem setOf_minimal_subset
deleted theorem isLowerSet_setOf
added theorem isLowerSet_setOfPred
deleted theorem isUpperSet_setOf
added theorem isUpperSet_setOfPred
deleted theorem isClosed_setOf_map_smul
deleted theorem isClosed_setOf_map_inv
deleted theorem isClosed_setOf_map_mul
deleted theorem isClosed_setOf_map_one
deleted theorem isClosed_setOf_clusterPt
deleted theorem IsClosed.setOf_mapsTo
modified theorem DiscreteQuotient.fiber_eq
deleted theorem Filter.isOpen_setOf_mem
deleted theorem IsGδ.setOf_continuousAt
modified def closedPoints
deleted theorem convex_setOf_holderOnWith
deleted theorem convex_setOf_holderWith
added theorem interior_setOfPred_eq
deleted theorem interior_setOf_eq
added theorem setOfPred_isOpen_iSup
added theorem setOfPred_isOpen_sSup
added theorem setOfPred_isOpen_sup
deleted theorem setOf_isOpen_iSup
deleted theorem setOf_isOpen_sSup
deleted theorem setOf_isOpen_sup