lift_lift_same_eq_lift — Mathlib

English

Under a compatibility condition on g, the lift commutes with iInf: (iInf f).lift g = iInf (f i).lift g.

Русский

При условии совместимости g с пересечением, подъём_Commutes с iInf: (iInf f).lift g = iInf (f i).lift g.

LaTeX

$$ (iInf f).lift g = ⨅ i, (f i).lift g$$

Lean4

theorem lift_lift_same_eq_lift {g : Set α → Set α → Filter β} (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_le_lift.antisymm <|
    le_lift.2 fun s hs =>
      le_lift.2 fun t ht =>
        lift_le (inter_mem hs ht) <|
          calc
            g (s ∩ t) (s ∩ t) ≤ g s (s ∩ t) := hg₂ (s ∩ t) inter_subset_left
            _ ≤ g s t := hg₁ s inter_subset_right

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