ker_prod

Mathlib.Order.Filter.Ker

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

English

The kernel of the product filter equals the product of kernels: ker (f ×ˢ g) = ker f ×ˢ ker g.

Русский

Ядро произведения фильтров равно произведению их ядер: ker(f × g) = ker f × ker g.

LaTeX

$$$\\ker (f \\times\\!\\, g) = \\ker f \\times\\!\\ker g$$$

Lean4

@[simp]
theorem ker_prod (f : Filter α) (g : Filter β) : ker (f ×ˢ g) = ker f ×ˢ ker g := by
  simp [Set.prod_eq, Filter.prod_eq_inf]

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

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

Разделы

Аффилиация

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