equicontinuousAt_unique — Mathlib

English

If ι has a single element, equicontinuity at x is equivalent to continuity of the unique F_i at x.

Русский

Если у индексного множества ровно одно значение, эконтинуальность в точке эквивалентна непрерывности единственной функции в этой точке.

LaTeX

$$$$ [Unique ι] \{F : ι \to X \to α\} {x : X} : EquicontinuousAt F x \iff ContinuousAt (F default) x. $$$$

Lean4

theorem equicontinuousAt_unique [Unique ι] {F : ι → X → α} {x : X} :
    EquicontinuousAt F x ↔ ContinuousAt (F default) x :=
  equicontinuousAt_finite.trans Unique.forall_iff

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