Commit 2026-10-13 14:51 ba9c63d0

View on Github →

refactor(Data): make Set a one-field structure (#41506) Replace

def Set (α : Type u) := α → Prop

with

structure Set (α : Type u) where
  ofPred :: Mem : α → Prop

Generated by Claude Opus. Painfully reviewed and improved line-by-line by myself. Fix #10941 Assisted-by: Claude Opus 4.8

Estimated changes

modified theorem NNReal.range_coe
modified theorem ManyOneDegree.add_of
modified def ManyOneDegree.of
modified theorem ManyOneDegree.of_eq_of
modified theorem ManyOneDegree.of_le_of
modified theorem manyOneReducible_toNat
modified theorem toNat_manyOneEquiv
modified theorem toNat_manyOneReducible
added theorem toNat_nat
modified theorem Finset.coe_eq_empty
modified theorem Finset.coe_eq_singleton
modified theorem Finset.coe_subset_singleton
modified theorem Finset.singleton_subset_coe
added def Set.memEquiv
modified theorem Set.ofPred_inj
modified theorem Set.ofPred_injective
added theorem Set.mem_eq_mem
deleted def Set.ofPred
added structure Set
deleted def Set
added theorem Measurable.mem
modified theorem measurable_set_iff
modified theorem measurable_set_mem
modified theorem AEMeasurable.mem
added theorem aemeasurable_comap_iff
modified theorem Set.compl_ne_eq_singleton
deleted def interPairsFilter
added def Set.memOrderIso
modified theorem Set.monotone_accumulate
modified theorem Set.subset_accumulate
modified theorem minimalPrimes_eq_minimals
modified theorem Metric.isBounded_of_abs_le
modified theorem Metric.isBounded_of_abs_lt
modified theorem nhdsKer_def
added theorem sdiff_mem_nhdsWithin