continuousAt_pi' — Mathlib

English

If for every i, ContinuousAt (λ y, f(y) i) x holds, then ContinuousAt f x.

Русский

Если для каждого i выполняется ContinuousAt (λ y, f(y) i) x, то ContinuousAt f x.

LaTeX

$$$$ \mathrm{ContinuousAt}(f, x) \Leftarrow \forall i, \mathrm{ContinuousAt}(\lambda y. f(y) i, x) $$$$

Lean4

@[fun_prop]
theorem continuousAt_pi' {f : X → ∀ i, A i} {x : X} (hf : ∀ i, ContinuousAt (fun y => f y i) x) : ContinuousAt f x :=
  continuousAt_pi.2 hf

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