English
Under a compatibility condition on g, lift commutes with iInf: (iInf f).lift g = iInf (f i).lift g.
Русский
При совместимости g с инфимумом подъёмы коммутируют: (iInf f).lift g = iInf (f i).lift g.
LaTeX
$$(iInf f).lift g = iInf (\lambda i => (f i).lift g)$$
Lean4
theorem lift_iInf [Nonempty ι] {f : ι → Filter α} {g : Set α → Filter β} (hg : ∀ s t, g (s ∩ t) = g s ⊓ g t) :
(iInf f).lift g = ⨅ i, (f i).lift g :=
by
refine lift_iInf_le.antisymm fun s => ?_
have H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t := by
intro t ht
refine iInf_sets_induct ht ?_ fun hs ht => ?_
· inhabit ι
exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)
· rw [hg]
exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht
simp only [mem_lift_sets (Monotone.of_map_inf hg), exists_imp, and_imp]
exact fun t ht hs => H t ht hs
