smallSets_mono — Mathlib

English

SmallSets is monotone with respect to the filter order.

Русский

Малые множества монотонны по упорядочению фильтров.

LaTeX

$$$ @Monotone (@smallSets\\,\\alpha) $$$

Lean4

theorem smallSets_mono {s t : α → Set β} (ht : Tendsto t la lb.smallSets) (hst : ∀ᶠ x in la, s x ⊆ t x) :
    Tendsto s la lb.smallSets := by
  rw [tendsto_smallSets_iff] at ht ⊢
  exact fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)

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