English
Let f be a filter on α and g: Set α → Set α → Set β. If g is monotone in the second argument (for all s, t ↦ g s t is monotone) and in the first (for all t, s ↦ g s t is monotone), then (f.lift (s ↦ f.lift' (g s))) = f.lift' (s ↦ g s s).
Русский
Пусть f — фильтр на α и g: Set α → Set α → Set β. Если g монотонна по обоим аргументам, то (f.lift (s ↦ f.lift' (g s))) = f.lift' (s ↦ g s s).
LaTeX
$$$(f.lift (\\lambda s. f.lift'(g\\,s))) = f.lift'(\\lambda s. g\\,s\\,s)$$$
Lean4
theorem lift_lift'_same_eq_lift' {g : Set α → Set α → Set β} (hg₁ : ∀ s, Monotone fun t => g s t)
(hg₂ : ∀ t, Monotone fun s => g s t) : (f.lift fun s => f.lift' (g s)) = f.lift' fun s => g s s :=
lift_lift_same_eq_lift (fun s => monotone_principal.comp (hg₁ s)) fun t => monotone_principal.comp (hg₂ t)
