Commit 2025-10-29 14:06 15ee1d2a
View on Github →chore: mark measure_union_ne_top and friends with finiteness (#30967)
In some cases, add ≠ ∞ versions of existing < ∞ lemmas, and tag those with finiteness.
Use this to golf one proof by measurability using finiteness, which is the morally correct proof.
Motivated by #30966.