tendsto_left_nhds_uniformity

Mathlib.Topology.UniformSpace.Defs

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

English

Repeated entry: Tendsto (fun a' => (a, a')) from nhds a to 𝓤 α.

Русский

Повторное утверждение: сходимость в nhds a к 𝓤 α для отображения (a, a').

LaTeX

$$$ \mathrm{Tendsto} (\lambda a' \mapsto (a,a')) (\mathcal{N}(a)) (\mathcal{U}(\alpha))$$$

Lean4

theorem tendsto_left_nhds_uniformity {a : α} : Tendsto (fun a' => (a, a')) (𝓝 a) (𝓤 α) := fun _ => mem_nhds_left a

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

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

Разделы

Аффилиация

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