equicontinuousWithinAt_univ — Mathlib

English

On a space, equicontinuity within universal set univ is equivalent to equicontinuity at a point.

Русский

На пространстве эквиконтинуальность внутри вселенной равна эквиконтинуальности в точке.

LaTeX

$$@[simp] equicontinuousWithinAt_univ (F) (x0) : EquicontinuousWithinAt F univ x0 ↔ EquicontinuousAt F x0$$

Lean4

@[simp]
theorem equicontinuousWithinAt_univ (F : ι → X → α) (x₀ : X) :
    EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀ := by
  rw [EquicontinuousWithinAt, EquicontinuousAt, nhdsWithin_univ]

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