coeFun — Mathlib

English

If f is continuous within s at z, then z ↦ f(z) viewed as a function is continuous within s at z.

Русский

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

LaTeX

$$$\forall hf : ContinuousWithinAt f s z,\forall x,\ ContinuousWithinAt (\lambda z, ⇑(f z)) s z$$$

Lean4

protected nonrec theorem coeFun (hf : ContinuousWithinAt f s z) : ContinuousWithinAt (fun z ↦ ⇑(f z)) s z :=
  hf.coeFun

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