equicontinuousOn_univ — Mathlib

English

Equicontinuity on the whole space is equivalent to equicontinuity as a global property.

Русский

Эконтинуальность на всей пространстве эквивалентна глобальной эконтинуальности.

LaTeX

$$$$ \operatorname{EquicontinuityOn}(F, \mathrm{univ}) \iff \operatorname{Equicontinuous} F. $$$$

Lean4

theorem equicontinuousOn_univ (F : ι → X → α) : EquicontinuousOn F univ ↔ Equicontinuous F := by
  simp [EquicontinuousOn, Equicontinuous]

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