feat(data/real/ennreal): add ennreal.prod_lt_top (#5602)

Also add `with_top.can_lift`, `with_top.mul_lt_top`, and `with_top.prod_lt_top`.

Author: urkud

src/algebra/big_operators/order.lean

@@ -319,14 +319,18 @@ end finset
 
 namespace with_top
 open finset
-open_locale classical
+
+/-- A product of finite numbers is still finite -/
+lemma prod_lt_top [canonically_ordered_comm_semiring β] [nontrivial β] [decidable_eq β]
+  {s : finset α} {f : α → with_top β} :
+  (∀a∈s, f a < ⊤) → (∏ x in s, f x) < ⊤ :=
+λ h, prod_induction f (λ a, a < ⊤) (λ a b, mul_lt_top) (coe_lt_top 1) h
 
 /-- A sum of finite numbers is still finite -/
 lemma sum_lt_top [ordered_add_comm_monoid β] {s : finset α} {f : α → with_top β} :
   (∀a∈s, f a < ⊤) → (∑ x in s, f x) < ⊤ :=
 λ h, sum_induction f (λ a, a < ⊤) (by { simp_rw add_lt_top, tauto }) zero_lt_top h
 
-
 /-- A sum of finite numbers is still finite -/
 lemma sum_lt_top_iff [canonically_ordered_add_monoid β] {s : finset α} {f : α → with_top β} :
   (∑ x in s, f x) < ⊤ ↔ (∀a∈s, f a < ⊤) :=

src/algebra/ordered_ring.lean

@@ -1043,4 +1043,11 @@ instance [nontrivial α] : canonically_ordered_comm_semiring (with_top α) :=
   .. with_top.canonically_ordered_add_monoid,
   .. with_top.no_zero_divisors, .. with_top.nontrivial }
 
+lemma mul_lt_top [nontrivial α] {a b : with_top α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ :=
+begin
+  lift a to α using ne_top_of_lt ha,
+  lift b to α using ne_top_of_lt hb,
+  simp only [← coe_mul, coe_lt_top]
+end
+
 end with_top

src/data/real/ennreal.lean

@@ -299,11 +299,11 @@ nat.le_induction (pow_one _) (λ m hm hm', by rw [pow_succ, hm', top_mul_top])
 lemma mul_eq_top : a * b = ∞ ↔ (a ≠ 0 ∧ b = ∞) ∨ (a = ∞ ∧ b ≠ 0) :=
 with_top.mul_eq_top_iff
 
-lemma mul_ne_top : a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞ :=
-by simp [(≠), mul_eq_top] {contextual := tt}
-
 lemma mul_lt_top  : a < ∞ → b < ∞ → a * b < ∞ :=
-by simpa only [ennreal.lt_top_iff_ne_top] using mul_ne_top
+with_top.mul_lt_top
+
+lemma mul_ne_top : a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞ :=
+by simpa only [lt_top_iff_ne_top] using mul_lt_top
 
 lemma ne_top_of_mul_ne_top_left (h : a * b ≠ ∞) (hb : b ≠ 0) : a ≠ ∞ :=
 by { simp [mul_eq_top, hb, not_or_distrib] at h ⊢, exact h.2 }
@@ -748,6 +748,10 @@ section sum
 
 open finset
 
+/-- A product of finite numbers is still finite -/
+lemma prod_lt_top {s : finset α} {f : α → ennreal} (h : ∀a∈s, f a < ∞) : (∏ a in s, f a) < ∞ :=
+with_top.prod_lt_top h
+
 /-- A sum of finite numbers is still finite -/
 lemma sum_lt_top {s : finset α} {f : α → ennreal} :
   (∀a∈s, f a < ∞) → ∑ a in s, f a < ∞ :=

src/order/bounded_lattice.lean

@@ -651,6 +651,11 @@ by simp [(≤)]
   @has_lt.lt (with_top α) _ (some a) none :=
 by simp [(<)]; existsi a; refl
 
+instance : can_lift (with_top α) α :=
+{ coe := coe,
+  cond := λ r, r ≠ ⊤,
+  prf := λ x hx, ⟨option.get $ option.ne_none_iff_is_some.1 hx, option.some_get _⟩ }
+
 instance [preorder α] : preorder (with_top α) :=
 { le          := λ o₁ o₂ : option α, ∀ a ∈ o₂, ∃ b ∈ o₁, b ≤ a,
   lt          := (<),