isBoundedUnder_comp — Mathlib

English

If there is hv: ∀ a0 a1, r a0 a1 → q (v a0) (v a1), then 𝓕 IsBoundedUnder r f implies 𝓕 IsBoundedUnder q (f ∘ φ).

Русский

Если существует hv: для всех a0,a1, r a0 a1 → q (v a0) (v a1), то 𝓕.IsBoundedUnder r f ⇒ 𝓕.IsBoundedUnder q (f ∘ φ).

LaTeX

$$$ hv : \forall a0 a1, r a0 a1 \Rightarrow q (v a0) (v a1) \Rightarrow 𝓕.IsBoundedUnder r f \Rightarrow 𝓕.IsBoundedUnder q (f \circ φ) $$$

Lean4

theorem isBoundedUnder_comp {ι κ X : Type*} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter ι} {𝓖 : Filter κ}
    (φ_tendsto : Tendsto φ 𝓖 𝓕) (𝓕_bounded : 𝓕.IsBoundedUnder r f) : 𝓖.IsBoundedUnder r (f ∘ φ) :=
  isBoundedUnder_map_iff.mp (𝓕_bounded.mono φ_tendsto)

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