lift_lift'_assoc — Mathlib

English

The composition of lift with lift' satisfies an associativity: (f.lift' g).lift h = f.lift (s ↦ (𝓟(g s)).lift h).

Русский

Сочетательность lift′ и lift: (f.lift' g).lift h = f.lift( s ↦ (𝓟(g s)).lift h ).

LaTeX

$$$ (f.lift' g).lift h = f.lift \\; (\\lambda s. (\\mathcal{P}(g s)).lift h) $$$

Lean4

theorem lift_lift'_assoc {g : Set α → Set β} {h : Set β → Filter γ} (hg : Monotone g) (hh : Monotone h) :
    (f.lift' g).lift h = f.lift fun s => h (g s) :=
  calc
    (f.lift' g).lift h = f.lift fun s => (𝓟 (g s)).lift h := lift_assoc (monotone_principal.comp hg)
    _ = f.lift fun s => h (g s) := by simp only [lift_principal, hh]

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