monotone_lift' — Mathlib

English

If f is monotone in γ and g is monotone in Set α → Set β, then c ↦ (f c).lift' (g c) is monotone.

Русский

Если f монотонно зависит от c и g монотонно, то c ↦ (f c).lift' (g c) монотонно по c.

LaTeX

$$$ \\text{monotone_lift'} \\ (hf : Monotone f) (hg : Monotone g) : \\text{Monotone } c \\mapsto (f c).lift' (g c) $$$

Lean4

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

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