eval_const — Mathlib

English

The coe function associated to continuous evaluation yields a continuous map from F to X-valued functions on α.

Русский

Связанный коэффициент функций непрерывной оценки порождает непрерывное отображение из F в функции α → X.

LaTeX

$$continuous_coeFun : Continuous (DFunLike.coe : F → α → X)$$

Lean4

@[continuity, fun_prop]
protected theorem eval_const (hf : Continuous f) (x : α) : Continuous (f · x) :=
  (continuous_eval_const x).comp hf

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