eval_const — Mathlib

English

If f is continuous within s at z, then for every x, f · x is continuous within s at z.

Русский

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

LaTeX

$$$\forall hf : ContinuousWithinAt f s z,\forall x : \alpha,\ ContinuousWithinAt (f \cdot x) s z$$$

Lean4

protected nonrec theorem eval_const (hf : ContinuousWithinAt f s z) (x : α) : ContinuousWithinAt (f · x) s z :=
  hf.eval_const x

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