pure_mul_pure — Mathlib

English

The product of two pure filters equals the pure filter of the product of their elements: pure a * pure b = pure (a * b).

Русский

Произведение двух чистых фильтров равно чистому фильтру от произведения элементов: pure a * pure b = pure (a b).

LaTeX

$$$$ \text{pure } a * \text{pure } b = \text{pure } (a \cdot b). $$$$

Lean4

@[to_additive]
theorem pure_mul_pure : (pure a : Filter α) * pure b = pure (a * b) := by simp

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