map_lift'_eq — Mathlib

English

If hh is monotone, then map m (f.lift' h) = f.lift' (image m ∘ h).

Русский

Если hh монотонно, то отображение m фильтра f.lift' h равно f.lift'(image m ∘ h).

LaTeX

$$$ (hh : Monotone h) :\\map m (f.lift' h) = f.lift' (\\mathrm{image}\\ m \\circ h) $$$

Lean4

theorem map_lift'_eq {m : β → γ} (hh : Monotone h) : map m (f.lift' h) = f.lift' (image m ∘ h) :=
  calc
    map m (f.lift' h) = f.lift (map m ∘ 𝓟 ∘ h) := map_lift_eq <| monotone_principal.comp hh
    _ = f.lift' (image m ∘ h) := by simp only [comp_def, Filter.lift', map_principal]

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