comap_eq_lift'

Mathlib.Order.Filter.Lift

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

English

For any m: α → β and any f: Filter β, comap m f equals f.lift' (preimage m).

Русский

Для отображения m: α → β и фильтра f на β, comap m f = f.lift' (preimage m).

LaTeX

$$$\\mathrm{comap}\\, m\\, f = f.lift' (\\mathrm{preimage}\\, m)$$$

Lean4

theorem comap_eq_lift' {f : Filter β} {m : α → β} : comap m f = f.lift' (preimage m) :=
  Filter.ext fun _ => (mem_lift'_sets monotone_preimage).symm

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

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

Разделы

Аффилиация

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