lift_iInf_le — Mathlib

English

If f is directed by ≥, and g is monotone, then (iInf f).lift g = ⨅ i, (f i).lift g.

Русский

Если f направлен по отношению ≥, а g монотонно, то (iInf f).lift g = ⨅ i, (f i).lift g.

LaTeX

$$Directed (\ge) f ∧ Monotone g ⇒ (iInf f).lift g = ⨅ i, (f i).lift g$$

Lean4

theorem lift_iInf_le {f : ι → Filter α} {g : Set α → Filter β} : (iInf f).lift g ≤ ⨅ i, (f i).lift g :=
  le_iInf fun _ => lift_mono (iInf_le _ _) le_rfl

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