eval — Mathlib

English

If f and g are continuous within a set s at z, then z ↦ f(z)(g(z)) is continuous within s at z.

Русский

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

LaTeX

$$$\\text{ContinuousWithinAt } f s z \\Rightarrow \\text{ContinuousWithinAt } g s z \\Rightarrow \\text{ContinuousWithinAt } (\\lambda z. f(z)(g(z))) s z$$$

Lean4

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

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