mono — Mathlib

English

If TendstoLocallyUniformlyOn F f p s holds and s' ⊆ s, then TendstoLocallyUniformlyOn F f p s'.

Русский

Если существует локальная равномерная сходимость на s и s' ⊆ s, то она сохраняется на s'.

LaTeX

$$$$\operatorname{TendstoLocallyUniformlyOn}(F,f,p,s) \Rightarrow (s'\subseteq s) \Rightarrow \operatorname{TendstoLocallyUniformlyOn}(F,f,p,s').$$$$

Lean4

theorem mono (h : TendstoLocallyUniformlyOn F f p s) (h' : s' ⊆ s) : TendstoLocallyUniformlyOn F f p s' :=
  by
  intro u hu x hx
  rcases h u hu x (h' hx) with ⟨t, ht, H⟩
  exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩

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