chore: generalize upcrossing lemmas#39645

RemyDegenne wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

RemyDegenne:RD_discreteIndexRemyDegenne/mathlib4:RD_discreteIndexCopy head branch name to clipboard