map_comm

Mathlib.Order.Filter.Map

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

English

The notational bind for Filter satisfies f >>= m = bind f m.

Русский

Обозначение бинда для Filter удовлетворяет f >>= m = bind f m.

LaTeX

$$$ f \gg= m = \mathrm{bind}(f,m) $$$

Lean4

theorem map_comm (H : ψ ∘ φ = ρ ∘ θ) (F : Filter α) : map ψ (map φ F) = map ρ (map θ F) := by
  rw [Filter.map_map, H, ← Filter.map_map]

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

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

Разделы

Аффилиация

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