Commit 2026-07-20 01:34 169c26b5

View on Github →

refactor: rename restrict to domRestrict (#25980) Update the documentation for consistency, and to contrast with codRestrict which is prevalent.

Estimated changes

deleted theorem MonoidHom.ker_restrict
deleted theorem MonoidHom.restrict_range
modified def MonoidHom.restrict
deleted theorem MonoidHom.restrict_apply
deleted theorem MonoidHom.restrict_mker
deleted theorem MonoidHom.restrict_mrange
modified def Submonoid.prod
deleted def MulHom.restrict
deleted theorem MulHom.restrict_apply
deleted theorem RingHom.restrict_apply
modified theorem cfcₙ_apply
modified theorem cfc_apply
deleted theorem Finset.restrict_preimage
added theorem strictMono_domRestrict
deleted theorem strictMono_restrict
deleted theorem Set.codRestrict_restrict
added def Set.domRestrict
added theorem Set.domRestrict_apply
added theorem Set.domRestrict_def
added theorem Set.domRestrict_dite
added theorem Set.domRestrict_eq
added theorem Set.domRestrict_eq_iff
added theorem Set.domRestrict_id
added theorem Set.domRestrict_ite
added theorem Set.domRestrict₂_def
added theorem Set.eq_domRestrict_iff
deleted theorem Set.eq_restrict_iff
added theorem Set.image_domRestrict
deleted theorem Set.image_restrict
modified theorem Set.injOn_iff_injective
added theorem Set.range_domRestrict
deleted theorem Set.range_restrict
deleted def Set.restrict
deleted theorem Set.restrict_apply
deleted theorem Set.restrict_def
deleted theorem Set.restrict_dite
deleted theorem Set.restrict_dite_compl
deleted theorem Set.restrict_eq
deleted theorem Set.restrict_eq_iff
deleted theorem Set.restrict_extend_range
deleted theorem Set.restrict_id
deleted theorem Set.restrict_ite
deleted theorem Set.restrict_ite_compl
deleted theorem Set.restrict_piecewise
deleted def Set.restrict₂
deleted theorem Set.restrict₂_def
modified theorem Set.surjOn_iff_surjective
deleted theorem Set.dependsOn_restrict
modified theorem Set.measurable_restrict
modified def Preorder.restrictLe
modified def AlgHom.extendScalars
modified theorem hasProd_singleton
deleted theorem IsClosedMap.restrict
added theorem IsOpenMap.domRestrict
deleted theorem IsOpenMap.restrict
deleted theorem Pi.continuous_restrict
deleted theorem Pi.continuous_restrict₂
added theorem Pi.induced_domRestrict
deleted theorem Pi.induced_restrict
modified theorem ContinuousMap.coe_restrict
modified theorem HolderWith.restrict_iff