tendstoUniformlyOn_iff_restrict — Mathlib

English

For any subset K, TendstoUniformlyOn F f p K is equivalent to TendstoUniformly (K.restrict F_n) (K.restrict f) p.

Русский

Для подмножества K равномерная сходимость эквивалентна равномерной сходимости после ограничения.

LaTeX

$$$${TendstoUniformlyOn F f p K} \\iff {TendstoUniformly (\\lambda n:\\, x\\in K. F n x) (K.restrict f) p}.$$$$

Lean4

theorem tendstoUniformlyOn_iff_restrict {K : Set α} :
    TendstoUniformlyOn F f p K ↔ TendstoUniformly (fun n : ι => K.restrict (F n)) (K.restrict f) p :=
  tendstoUniformlyOn_iff_tendstoUniformly_comp_coe

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