EquicontinuousWithinAt — Mathlib

English

If F is equicontinuous at x0 on a set T, and S ⊆ T, then F is equicontinuous at x0 on S.

Русский

Если F эквиконтинуально в точке x0 на T, и S ⊆ T, тогда F эквиконтинуально на S.

LaTeX

$$$\text{EquicontinuousWithinAt}(F,T,x_0) \land S \subseteq T \Rightarrow \text{EquicontinuousWithinAt}(F,S,x_0)$$$

Lean4

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

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