uniformEquicontinuous_finite

Mathlib.Topology.UniformSpace.Equicontinuity

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

Lean4

theorem uniformEquicontinuous_finite [Finite ι] {F : ι → β → α} :
    UniformEquicontinuous F ↔ ∀ i, UniformContinuous (F i) := by
  simp only [UniformEquicontinuous, eventually_all, @forall_swap _ ι]; rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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