inner — Mathlib

English

The map x ↦ unitBall x is C^n smooth (in the real sense) when viewed through a homeomorphism (unitBall).

Русский

Карта x ↦ unitBall x гладкая до порядка n в рамках соответствующего гомеоморфа.

LaTeX

$$$\\text{ContDiff}_{\\mathbb{R}}^{n}\\big(\\mathrm{unitBall}\\big)$$$

Lean4

theorem inner {f g : α → E} {l : Filter α} {x y : E} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
    Tendsto (fun t => ⟪f t, g t⟫) l (𝓝 ⟪x, y⟫) :=
  (continuous_inner.tendsto _).comp (hf.prodMk_nhds hg)

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