chore(measure_theory/function/lp_space): move `fact`s (#11107)
Move from `measure_theory/function/lp_space` to `data/real/ennreal` the `fact`s
- `fact_one_le_one_ennreal`
- `fact_one_le_two_ennreal`
- `fact_one_le_top_ennreal`
so that they can be used not just in the measure theory development of `Lp` space but also in the new `lp` spaces.
