continuousOn_of_mem

Mathlib.Topology.UniformSpace.Equicontinuity

URI: https://scilib.ai/kg/mathlib#Set.EquicontinuousOn.continuousOn_of_mem

← MathLib Explorer

English

If H is equicontinuous on S and f ∈ H, then f is continuous on S.

Русский

Если H равноконтинуально на S и f ∈ H, то f непрерывна на S.

LaTeX

$$$f \\in H \\Rightarrow f|_S \\in C(S, α)$$$

Lean4

protected theorem continuousOn_of_mem {H : Set <| X → α} {S : Set X} (h : H.EquicontinuousOn S) {f : X → α}
    (hf : f ∈ H) : ContinuousOn f S :=
  h.continuousOn ⟨f, hf⟩

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

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

Разделы

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

Аффилиация

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