uniformEquicontinuousOn_unique — Mathlib

English

Let ι be a type with a unique element i0. For any F : ι → β → α and any S ⊆ β, the family F is uniformly equicontinuous on S if and only if the single function F(i0) is uniformly continuous on S.

Русский

Пусть ι — тип с единственным элементом i0. Для любой F : ι → β → α и любого множества S ⊆ β семействo функций {F(i)} на S является равномерно эконтинуальным, тогда и только если единственная функция F(i0) равномерно непрерывна на S.

LaTeX

$$$\text{UniformEquicontinuousOn}(F,S) \iff \text{UniformContinuousOn}(F(i_0),S)$$$

Lean4

theorem uniformEquicontinuousOn_unique [Unique ι] {F : ι → β → α} {S : Set β} :
    UniformEquicontinuousOn F S ↔ UniformContinuousOn (F default) S :=
  uniformEquicontinuousOn_finite.trans Unique.forall_iff

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