EquicontinuousAt — Mathlib

English

For a set H of functions F: X → α, equicontinuity at x0 for the family is equivalent to equicontinuity of the lifted map (↑) : H → X → α at x0.

Русский

Для множества H функций эквиконтинуальность в точке x0 той же самой семейства эквивалентна эквиконтинуальности отображения (↑): H → X → α в точке x0.

LaTeX

$$$EquicontinuousAt(H,x_0) \equiv EquicontinuousAt((↑):H→X→α,x_0)$$$

Lean4

/-- We say that a set `H : Set (X → α)` of functions is equicontinuous at a point if the family
`(↑) : ↥H → (X → α)` is equicontinuous at that point. -/
protected abbrev EquicontinuousAt (H : Set <| X → α) (x₀ : X) : Prop :=
  EquicontinuousAt ((↑) : H → X → α) x₀

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