equicontinuousAt_finite — Mathlib

English

If the index set ι is finite, then equicontinuity at x0 is equivalent to all F_i being continuous at x0.

Русский

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

LaTeX

$$$$ [Finite ι]\ EquicontinuousAt F x_0 \iff \forall i, ContinuousAt (F i) x_0. $$$$

Lean4

theorem equicontinuousAt_finite [Finite ι] {F : ι → X → α} {x₀ : X} :
    EquicontinuousAt F x₀ ↔ ∀ i, ContinuousAt (F i) x₀ := by
  simp [EquicontinuousAt, ContinuousAt, (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff, UniformSpace.ball,
    @forall_swap _ ι]

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