mono — Mathlib

English

If v ≤ u, a TendstoInMeasure statement for f is preserved when passing to a smaller filter v.

Русский

Если v ≤ u, то справедливо сохранение TendstoInMeasure при переходе к меньшему фильтру.

LaTeX

$$$TendstoInMeasure μ f v g := (TendstoInMeasure μ f u g).mono_left v u$$$

Lean4

theorem mono [EDist E] {f : ι → α → E} {g : α → E} {u v : Filter ι} (huv : v ≤ u) (hg : TendstoInMeasure μ f u g) :
    TendstoInMeasure μ f v g := fun ε hε => (hg ε hε).mono_left huv

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