equicontinuousWithinAt_empty — Mathlib

English

Similarly, if indices are empty, equicontinuous within any set S at x0 is automatic.

Русский

Аналогично, если индексов пусто, то эконтинуальность внутри любого множества достигается автоматически.

LaTeX

$$$$ [|\iota|=0]\Rightarrow \operatorname{EquicontinuousWithinAt}(F, S, x_0). $$$$

Lean4

@[simp]
theorem equicontinuousWithinAt_empty [h : IsEmpty ι] (F : ι → X → α) (S : Set X) (x₀ : X) :
    EquicontinuousWithinAt F S x₀ := fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

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