equicontinuousWithinAt_finite — Mathlib

English

If ι is finite, equicontinuity within S at x0 is equivalent to all F_i being continuous within S at x0.

Русский

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

LaTeX

$$$$ [Finite ι]\ EquicontinuousWithinAt F S x_0 \iff \forall i, ContinuousWithinAt (F i) S x_0. $$$$

Lean4

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

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