lift_map_le — Mathlib

English

The lift of the mapped filter is bounded by the original lift: (map m f).lift g ≤ f.lift (g ∘ image m).

Русский

Подъем образованного фильтра ограничивает исходный подъём: (map m f).lift g ≤ f.lift (g ∘ image m).

LaTeX

$$(map m f).lift g ≤ f.lift (g \circ image m)$$

Lean4

theorem lift_map_le {g : Set β → Filter γ} {m : α → β} : (map m f).lift g ≤ f.lift (g ∘ image m) :=
  le_lift.2 fun _s hs => lift_le (image_mem_map hs) le_rfl

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