Theorems · Theorem · general topology

ENNReal.Tendsto.mul

∀ {α : Type u_1} {f : Filter α} {ma mb : α → ENNReal} {a b : ENNReal},
  Filter.Tendsto ma f (nhds a) →
    a ≠ 0 ∨ b ≠ ⊤ →
      Filter.Tendsto mb f (nhds b) → b ≠ 0 ∨ a ≠ ⊤ → Filter.Tendsto (fun a => ma a * mb a) f (nhds (a * b))

Defined in

Mathlib.Topology.Instances.ENNReal.Lemmas

Cited by

9 results in Mathlib

Foundations

Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound