mono — Mathlib

English

If a family tends uniformly on a set s, it also tends uniformly on any subset s' ⊆ s.

Русский

Если семейство сходится по равномерности на s, то аналогично на любом подмножестве s' ⊆ s.

LaTeX

$$$h : TendstoUniformlyOn F f p s \\quad \\text{and} \\quad s' \\subseteq s \\Rightarrow TendstoUniformlyOn F f p s'$$$

Lean4

theorem mono (h : TendstoUniformlyOn F f p s) (h' : s' ⊆ s) : TendstoUniformlyOn F f p s' :=
  tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr
    (h.tendstoUniformlyOnFilter.mono_right (le_principal_iff.mpr <| mem_principal.mpr h'))

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