continuousAt — Mathlib

English

If a family is equicontinuous at x0, then each member is continuous at x0.

Русский

Если семейство экконтинуально в точке x0, то каждый элемент непрерывен в x0.

LaTeX

$$$\text{EquicontinuousAt } F x_0 \Rightarrow \forall i, \text{ContinuousAt } (F_i) x_0$$$

Lean4

/-- Each function of a family equicontinuous at `x₀` is continuous at `x₀`. -/
theorem continuousAt {F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (i : ι) : ContinuousAt (F i) x₀ :=
  (UniformSpace.hasBasis_nhds _).tendsto_right_iff.2 fun U ⟨hU, _⟩ ↦ (h U hU).mono fun _x hx ↦ hx i

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