uniformEquicontinuousOn_empty — Mathlib

English

Similarly, a universally empty index yields uniform equicontinuity on any S.

Русский

Аналогично, пустой индекс дает униформную эконтинуальность на любом S.

LaTeX

$$$$ [IsEmpty ι] (F : ι → β → α) (S : Set β) \Rightarrow \operatorname{UniformEquicontinuousOn} F S. $$$$

Lean4

@[simp]
theorem uniformEquicontinuousOn_empty [h : IsEmpty ι] (F : ι → β → α) (S : Set β) : UniformEquicontinuousOn F S :=
  fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

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