map_lift'_eq2

Mathlib.Order.Filter.Lift

URI: https://scilib.ai/kg/mathlib#Filter.map_lift'_eq2

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$ (hg : Monotone g) : (map m f).lift' g = f.lift' (g \\circ image m) $$$

Lean4

theorem map_lift'_eq2 {g : Set β → Set γ} {m : α → β} (hg : Monotone g) : (map m f).lift' g = f.lift' (g ∘ image m) :=
  map_lift_eq2 <| monotone_principal.comp hg

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

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

Разделы

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

Аффилиация

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