monotone_lift — Mathlib

English

If f and g are monotone in their respective domains, then c ↦ (f(c)).lift (g(c)) is monotone.

Русский

Если f и g монотонны по отношению к своим переменным, то c ↦ (f(c)).lift (g(c)) монотонно.

LaTeX

$$Monotone f \rightarrow Monotone g \rightarrow Monotone (c \mapsto (f c).lift (g c))$$

Lean4

theorem monotone_lift [Preorder γ] {f : γ → Filter α} {g : γ → Set α → Filter β} (hf : Monotone f) (hg : Monotone g) :
    Monotone fun c => (f c).lift (g c) := fun _ _ h => lift_mono (hf h) (hg h)

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