Commit 2026-02-23 17:11 4166dc3b
View on Github →feat(Order/CompactlyGenerated): remove injectivity hypothesis in iSupIndep_iff_supIndep_of_injOn (#35475)
The theorem iSupIndep_iff_supIndep_of_injOn asks for an injectivity hypothesis which is redundant. It has been removed.
I have renamed iSupIndep_iff_supIndep_of_injOn to iSupIndep_iff_supIndep. The preexisting theorem iSupIndep_iff_supIndep has been renamed to iSupIndep_comp_coe_iff_supIndep which I believe is more accurate.
Note: The name clash means we can't deprecate iSupIndep_iff_supIndep (to the best of my knowledge), but I think it's worth it since the new iSupIndep_iff_supIndep is now what I would expect it to be.