equicontinuousOn_finite — Mathlib

English

For finite ι, equicontinuity on S is equivalent to each F_i being continuous on S.

Русский

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

LaTeX

$$$$ [Finite ι]\ EquicontinuousOn F S \iff \forall i, ContinuousOn (F i) S. $$$$

Lean4

theorem equicontinuousOn_finite [Finite ι] {F : ι → X → α} {S : Set X} :
    EquicontinuousOn F S ↔ ∀ i, ContinuousOn (F i) S := by
  simp only [EquicontinuousOn, equicontinuousWithinAt_finite, ContinuousOn, @forall_swap ι]

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