Theorem measure_theory.exists_integrable_pos_of_sigma_finite

chore(data/real/ennreal, measure_theory/): use `≠ ∞` and `≠ 0` in assumptions (#9219)

feat(measure_theory/integration): in a sigma finite space, there exists an integrable positive function (#7721)