map_lift_eq2

Mathlib.Order.Filter.Lift

URI: https://scilib.ai/kg/mathlib#Filter.map_lift_eq2

← MathLib Explorer

English

If g is monotone then (map m f).lift g = f.lift (g ∘ image m).

Русский

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

LaTeX

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

Lean4

theorem map_lift_eq2 {g : Set β → Filter γ} {m : α → β} (hg : Monotone g) : (map m f).lift g = f.lift (g ∘ image m) :=
  lift_map_le.antisymm <| le_lift.2 fun _s hs => lift_le hs <| hg <| image_preimage_subset _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru