prodMap — Mathlib

English

If f is continuous at p.fst and g is continuous at p.snd, then Prod.map f g is continuous at p.

Русский

Если f непрерывна в p.fst, а g в p.snd, то Prod.map f g непрерывна в p.

LaTeX

$$$ (ContinuousAt f p.fst) \\land (ContinuousAt g p.snd) \\Rightarrow ContinuousAt (Prod.map f g) p $$$

Lean4

theorem prodMap {f : X → Z} {g : Y → W} {p : X × Y} (hf : ContinuousAt f p.fst) (hg : ContinuousAt g p.snd) :
    ContinuousAt (Prod.map f g) p :=
  hf.fst''.prodMk hg.snd''

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