eval — Mathlib

English

If f is continuous at z and g is continuous at z, then the evaluation map z ↦ f(z)(g(z)) is continuous at z.

Русский

Если f и g непрерывны в z, то отображение z ↦ f(z)(g(z)) непрерывно в z.

LaTeX

$$$\\text{ContinuousAt } f z \\; \\&\\; \\text{ContinuousAt } g z \\Rightarrow \\text{ContinuousAt } (\\lambda z. f(z)(g(z))) z$$$

Lean4

protected nonrec theorem eval (hf : ContinuousAt f z) (hg : ContinuousAt g z) : ContinuousAt (fun z ↦ f z (g z)) z :=
  hf.eval hg

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