Commit 2021-12-25 16:16 914250ef

chore(data/real/ennreal): adjust form of to_real_pos_iff (#11047) We have a principle (which may not have been crystallized at the time of writing of data/real/ennreal) that hypotheses of lemmas should contain the weak form a ≠ ∞, while conclusions should report the strong form a < ∞, and also the same for a ≠ 0, 0 < a. In the case of the existing lemma

lemma to_real_pos_iff : 0 < a.to_real ↔ (0 < a ∧ a ≠ ∞):=

it's not clear whether the RHS of the iff should count as a hypothesis or a conclusion. So I have rewritten to provide two forms,

lemma to_real_pos_iff : 0 < a.to_real ↔ (0 < a ∧ a < ∞):=
lemma to_real_pos {a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ∞) : 0 < a.to_real :=

Having both versions available shortens many proofs slightly.