prodMap' — Mathlib

English

A variant of ContinuousAt.prodMap avoiding explicit fst/snd by using the same point (x,y).

Русский

Вариант ContinuousAt.prodMap без явного fst/snd, используя ту же точку (x,y).

LaTeX

$$$ (ContinuousAt f x) \\land (ContinuousAt g y) \\Rightarrow ContinuousAt (Prod.map f g) (x, y) $$$

Lean4

/-- A version of `ContinuousAt.prodMap` that avoids `Prod.fst`/`Prod.snd`
by assuming that the point is `(x, y)`. -/
theorem prodMap' {f : X → Z} {g : Y → W} {x : X} {y : Y} (hf : ContinuousAt f x) (hg : ContinuousAt g y) :
    ContinuousAt (Prod.map f g) (x, y) :=
  hf.prodMap hg

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