equicontinuous_finite — Mathlib

English

If ι is finite, equicontinuity of F is equivalent to all F_i being continuous.

Русский

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

LaTeX

$$$$ [Finite ι]\ Equicontinuous F \iff \forall i, Continuous (F i). $$$$

Lean4

theorem equicontinuous_finite [Finite ι] {F : ι → X → α} : Equicontinuous F ↔ ∀ i, Continuous (F i) := by
  simp only [Equicontinuous, equicontinuousAt_finite, continuous_iff_continuousAt, @forall_swap ι]

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