English
The lift operation commutes with a second lift: f.lift (s ↦ g.lift (h s)) = g.lift (t ↦ f.lift (h s t)).
Русский
Операция подъёма коммутирует с вторым подъёмом: f.lift (s ↦ g.lift (h s)) = g.lift (t ↦ f.lift (h s t)).
LaTeX
$$f.lift (\lambda s => g.lift (h s)) = g.lift (\lambda t => f.lift (\lambda s => h s t))$$
Lean4
theorem lift_comm {g : Filter β} {h : Set α → Set β → Filter γ} :
(f.lift fun s => g.lift (h s)) = g.lift fun t => f.lift fun s => h s t :=
le_antisymm
(le_iInf fun i =>
le_iInf fun hi =>
le_iInf fun j => le_iInf fun hj => iInf_le_of_le j <| iInf_le_of_le hj <| iInf_le_of_le i <| iInf_le _ hi)
(le_iInf fun i =>
le_iInf fun hi =>
le_iInf fun j => le_iInf fun hj => iInf_le_of_le j <| iInf_le_of_le hj <| iInf_le_of_le i <| iInf_le _ hi)
