comap_lift_eq2 — Mathlib

English

If g is monotone, then (comap m f).lift g = f.lift (g ∘ preimage m).

Русский

Если g монотонно, то (comap m f).lift g = f.lift (g ∘ preimage m).

LaTeX

$$ (comap m f).lift g = f.lift (g \circ preimage m)$$

Lean4

theorem comap_lift_eq2 {m : β → α} {g : Set β → Filter γ} (hg : Monotone g) :
    (comap m f).lift g = f.lift (g ∘ preimage m) :=
  le_antisymm (le_iInf₂ fun s hs => iInf₂_le (m ⁻¹' s) ⟨s, hs, Subset.rfl⟩)
    (le_iInf₂ fun _s ⟨s', hs', h_sub⟩ => iInf₂_le_of_le s' hs' <| hg h_sub)

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