continuousAt_pi

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#continuousAt_pi

English

ContinuousAt f x is equivalent to ∀ i, ContinuousAt (λ y, f(y) i) x.

Русский

ContinuousAt f x эквивалентно ∀ i, ContinuousAt (λ y, f(y) i) x.

LaTeX

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

Lean4

theorem continuousAt_pi {f : X → ∀ i, A i} {x : X} : ContinuousAt f x ↔ ∀ i, ContinuousAt (fun y => f y i) x :=
  tendsto_pi_nhds

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru