map₂_div

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.map₂_div

English

The division operation on filters coincides with the pointwise map of division: f / g = map₂ (× / ×) f g.

Русский

Операция деления фильтров совпадает с точечным отображением деления: f / g = map₂ (× / ×) f g.

LaTeX

$$$f / g = \\operatorname{map}_2 \\bigl(\\tfrac{\\cdot}{\\cdot}\\bigr) f g.$$$

Lean4

@[to_additive (attr := simp)]
theorem map₂_div : map₂ (· / ·) f g = f / g :=
  rfl

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

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

Разделы

Аффилиация

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