mono_right — Mathlib

English

If TendstoUniformlyOnFilter F f p p' holds and p'' ≤ p', then TendstoUniformlyOnFilter F f p p''.

Русский

Если TendstoUniformlyOnFilter выполняется для p→p' и p''≤p', то для p→p'' тоже верно.

LaTeX

$$$$\\text{TendstoUniformlyOnFilter}(F,f,p,p')\\land p''\\le p'\\Rightarrow \\text{TendstoUniformlyOnFilter}(F,f,p,p'').$$$$

Lean4

theorem mono_right {p'' : Filter α} (h : TendstoUniformlyOnFilter F f p p') (hp : p'' ≤ p') :
    TendstoUniformlyOnFilter F f p p'' := fun u hu => (h u hu).filter_mono (p.prod_mono_right hp)

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