const_mul — Mathlib

English

If f,g are continuous and the same nondegenerate conditions hold, then the product map is continuous.

Русский

Если f и g непрерывны и выполняются те же ненулевые условия, то произведение непрерывно.

LaTeX

$$$\\\\text{Continuous } f \\Rightarrow \\\\text{Continuous } g \\Rightarrow \\\\forall x, (f x ≠ 0 ∨ g x ≠ ∞) ∧ (g x ≠ 0 ∨ f x ≠ ∞) \\Rightarrow \\\\text{Continuous } (x \\mapsto f x * g x).$$$

Lean4

protected theorem const_mul {f : Filter α} {m : α → ℝ≥0∞} {a b : ℝ≥0∞} (hm : Tendsto m f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ∞) :
    Tendsto (fun b => a * m b) f (𝓝 (a * b)) :=
  by_cases (fun (this : a = 0) => by simp [this, tendsto_const_nhds]) fun ha : a ≠ 0 =>
    ENNReal.Tendsto.mul tendsto_const_nhds (Or.inl ha) hm hb

Похожие утверждения