lift_assoc — Mathlib

English

With Monotone g, lifting twice is the same as lifting by s ↦ (g s).lift h.

Русский

При монотонном g двойной подъём равен подъему по s ↦ (g s).lift h.

LaTeX

$$ (f.lift g).lift h = f.lift (\lambda s => (g s).lift h)$$

Lean4

theorem lift_assoc {h : Set β → Filter γ} (hg : Monotone g) : (f.lift g).lift h = f.lift fun s => (g s).lift h :=
  le_antisymm
    (le_iInf₂ fun _s hs => le_iInf₂ fun t ht => iInf_le_of_le t <| iInf_le _ <| (mem_lift_sets hg).mpr ⟨_, hs, ht⟩)
    (le_iInf₂ fun t ht =>
      let ⟨s, hs, h'⟩ := (mem_lift_sets hg).mp ht
      iInf_le_of_le s <| iInf_le_of_le hs <| iInf_le_of_le t <| iInf_le _ h')

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