lift_lift_same_le_lift — Mathlib

English

The lift of the infimum is bounded above by the infimum of lifts: (iInf f).lift g ≤ ⨅ i, (f i).lift g.

Русский

Подъем пространства пересечений ≤ пересечение подъемов: (iInf f).lift g ≤ ⨅ i, (f i).lift g.

LaTeX

$$(iInf f).lift g ≤ ⨅ i, (f i).lift g$$

Lean4

theorem lift_lift_same_le_lift {g : Set α → Set α → Filter β} :
    (f.lift fun s => f.lift (g s)) ≤ f.lift fun s => g s s :=
  le_lift.2 fun _s hs => lift_le hs <| lift_le hs le_rfl

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