UniformEquicontinuousOn — Mathlib

English

Uniform equicontinuity of a set of functions on a space β is defined via the lifted map (↑).

Русский

Равномерная эквиконтинуальность множества функций на пространстве β определяется через поднятое отображение (↑).

LaTeX

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

Lean4

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

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