mono_left — Mathlib

English

If hf is a UniformCauchySeqOnFilter and hp: p'' ≤ p, then UniformCauchySeqOnFilter F p'' p' holds.

Русский

Если hf — UniformCauchySeqOnFilter и hp: p'' ≤ p, то UniformCauchySeqOnFilter F p'' p' выполняется.

LaTeX

$$$hf \Rightarrow hp \Rightarrow UniformCauchySeqOnFilter F p'' p'$$$

Lean4

theorem mono_left {p'' : Filter ι} (hf : UniformCauchySeqOnFilter F p p') (hp : p'' ≤ p) :
    UniformCauchySeqOnFilter F p'' p' := fun u hu => (hf u hu).filter_mono (p'.prod_mono_left (Filter.prod_mono hp hp))

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