Commit 2021-09-11 22:57 55aaebe1

feat(data/real/ennreal): add contravariant_class ennreal ennreal (+) (<) (#9143)

algebra/ordered_monoid

• use ≠ ⊤/≠ ⊥ instead of < ⊤/⊥ < in the assumptions of with_top.add_lt_add_iff_left, with_top.add_lt_add_iff_right, with_bot.add_lt_add_iff_left, and with_bot.add_lt_add_iff_right;
• add instances for contravariant_class (with_top α) (with_top α) (+) (<) and contravariant_class (with_bot α) (with_bot α) (+) (<).

data/real/ennreal

• use ≠ ∞ instead of < ∞ in the assumptions of ennreal.add_lt_add_iff_left, ennreal.add_lt_add_iff_right, ennreal.lt_add_right,
• add an instance contravariant_class ℝ≥0∞ ℝ≥0∞ (+) (<);
• rename ennreal.sub_infty to ennreal.sub_top.

measure_theory/measure/outer_measure

• use ≠ ∞ instead of < ∞ in the assumptions of induced_outer_measure_exists_set;

topology/metric_space/emetric_space

• use ≠ ∞ instead of < ∞ in the assumptions of emetric.ball_subset.