tendstoUniformlyOn_empty

Mathlib.Topology.UniformSpace.UniformConvergence

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

English

Uniform convergence on the empty set is vacuously true for any F, f, p.

Русский

Равномерная сходимость на пустом множестве тождественна по всем F, f, p.

LaTeX

$$TendstoUniformlyOn F f p ∅$$

Lean4

/-- Uniform convergence on the empty set is vacuously true -/
theorem tendstoUniformlyOn_empty : TendstoUniformlyOn F f p ∅ := fun u _ => by simp

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

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

Разделы

Аффилиация

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