mul — Mathlib

English

If f and g are LocallyLipschitzOn on s, then their product is LocallyLipschitzOn on s.

Русский

Если f и g локально липшицевы на s, то их произведение также локально липшицево на s.

LaTeX

$$$\\mathrm{LocallyLipschitzOn}\\ s\\ f \\land \\mathrm{LocallyLipschitzOn}\\ s\\ g \\Rightarrow \\mathrm{LocallyLipschitzOn}\\ s\\ (\\lambda x. f(x)g(x)).$$$

Lean4

@[to_additive]
theorem mul (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) : LocallyLipschitzOn s fun x ↦ f x * g x :=
  fun x hx ↦ by
  obtain ⟨Kf, t, ht, hKf⟩ := hf hx
  obtain ⟨Kg, u, hu, hKg⟩ := hg hx
  exact ⟨Kf + Kg, t ∩ u, inter_mem ht hu, (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩

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