Commit 2024-10-04 14:05 eeedb316

View on Github →

chore(Data/Set): split Data/Set/Function (#17091) Take the lemmas about monotonicity of functions out of Data/Set/Function and move them to Data/Set/Monotone. Also remove Compl.decidableMem, as it is already given in decidableCompl (instance search already finds it too)

Estimated changes

deleted theorem AntitoneOn.congr
deleted theorem AntitoneOn.mono
deleted theorem MonotoneOn.congr
deleted theorem MonotoneOn.mono
deleted theorem Set.EqOn.congr_antitoneOn
deleted theorem Set.EqOn.congr_monotoneOn
deleted theorem StrictAntiOn.comp
deleted theorem StrictAntiOn.congr
deleted theorem StrictAntiOn.injOn
deleted theorem StrictAntiOn.mono
deleted theorem StrictMono.codRestrict
deleted theorem StrictMonoOn.comp
deleted theorem StrictMonoOn.congr
deleted theorem StrictMonoOn.injOn
deleted theorem StrictMonoOn.mono
deleted theorem strictMono_restrict
added theorem AntitoneOn.congr
added theorem AntitoneOn.mono
added theorem MonotoneOn.congr
added theorem MonotoneOn.mono
added theorem StrictAntiOn.comp
added theorem StrictAntiOn.congr
added theorem StrictAntiOn.injOn
added theorem StrictAntiOn.mono
added theorem StrictMono.codRestrict
added theorem StrictMonoOn.comp
added theorem StrictMonoOn.congr
added theorem StrictMonoOn.injOn
added theorem StrictMonoOn.mono
added theorem strictMono_restrict