equicontinuous_empty

Mathlib.Topology.UniformSpace.Equicontinuity

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

English

If the index set is empty, then the family is equicontinuous.

Русский

Если индекс пуст, то семейство эконтинуально.

LaTeX

$$$$ [IsEmpty ι] \Rightarrow \operatorname{Equicontinuous} F. $$$$

Lean4

@[simp]
theorem equicontinuous_empty [IsEmpty ι] (F : ι → X → α) : Equicontinuous F :=
  equicontinuousAt_empty F

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

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

Разделы

Аффилиация

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