lift_iInf_of_directed — Mathlib

English

If g maps univ to top and g is compatible, then (iInf f).lift g = iInf (f i).lift g.

Русский

Если g(univ) = ⊤ и совместима, то (iInf f).lift g = iInf (f i).lift g.

LaTeX

$$hg' : g univ = ⊤ ∧ hg : ∀ s t, g (s ∩ t) = g s ⊓ g t ⇒ (iInf f).lift g = iInf i, (f i).lift g$$

Lean4

theorem lift_iInf_of_directed [Nonempty ι] {f : ι → Filter α} {g : Set α → Filter β} (hf : Directed (· ≥ ·) f)
    (hg : Monotone g) : (iInf f).lift g = ⨅ i, (f i).lift g :=
  lift_iInf_le.antisymm fun s =>
    by
    simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]
    exact fun t i ht hs => mem_iInf_of_mem i <| mem_lift ht hs

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