rmap_sets

Mathlib.Order.Filter.Partial

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

English

The sets of the rmap filter are exactly the preimages of l.sets under r.core.

Русский

Множества фильтра rmap совпадают с предобразами множества l.sets под действием r.core.

LaTeX

$$$(l.rmap r).sets = r.core^{-1}'(l.sets)$$$

Lean4

theorem rmap_sets (r : SetRel α β) (l : Filter α) : (l.rmap r).sets = r.core ⁻¹' l.sets :=
  rfl

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

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

Разделы

Аффилиация

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