eval_const — Mathlib

English

If f is continuous within s at z, then the function z ↦ f(z) is continuous within s at z, when viewed as a function into α → X.

Русский

Если f непрерывна внутри s в z, то функция z ↦ f(z) непрерывна внутри s в z, воспринимаемая как функция в α → X.

LaTeX

$$$\forall hf : ContinuousWithinAt f s z,\ ContinuousWithinAt (\lambda z, inst.coe (f z)) s z$$$

Lean4

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

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