EquicontinuousOn — Mathlib

English

A set H of functions is uniformly equicontinuous if the lifted family is uniformly equicontinuous.

Русский

Множество функций эквиконтинуально равномерно, если соответствующее отображение эквиконтинуально равномерно.

LaTeX

$$UniformEquicontinuous((↑) : H → β → α)$$

Lean4

/-- We say that a set `H : Set (X → α)` of functions is equicontinuous on a subset if the family
`(↑) : ↥H → (X → α)` is equicontinuous on that subset. -/
protected abbrev EquicontinuousOn (H : Set <| X → α) (S : Set X) : Prop :=
  EquicontinuousOn ((↑) : H → X → α) S

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