coeFun — Mathlib

English

If f is continuous on s, then for every x, the map z ↦ f(z)(x) is continuous on s.

Русский

Если f непрерывна на s, то для каждого x отображение z ↦ f(z)(x) непрерывно на s.

LaTeX

$$$\forall f : Z \to F,\ ContinuousOn f s \Rightarrow \forall x,\ ContinuousOn (\lambda z, (f z) x) s$$$

Lean4

protected theorem coeFun (hf : ContinuousOn f s) (x : α) : ContinuousOn (f · x) s := fun z hz ↦ (hf z hz).eval_const x

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