equicontinuous_unique — Mathlib

English

For a unique index set, equicontinuity of F is equivalent to continuity of the unique F_i.

Русский

Для уникального индекса эконтинуальность F эквивалентна непрерывности единственной F_i.

LaTeX

$$$$ [Unique ι] \{F : ι \to X \to α\} : \operatorname{Equicontinuous} F \iff \operatorname{Continuous}(F default). $$$$

Lean4

theorem equicontinuous_unique [Unique ι] {F : ι → X → α} : Equicontinuous F ↔ Continuous (F default) :=
  equicontinuous_finite.trans Unique.forall_iff

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