pure_smul_pure — Mathlib

English

The product of two pure filters is the pure filter of the product of the points, i.e., (pure a) • (pure b) = pure (a • b).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem pure_smul_pure : (pure a : Filter α) • (pure b : Filter β) = pure (a • b) := by simp

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