pure_vsub_pure — Mathlib

English

The vsub of two principal filters is the principal filter of their vsub: (pure a) -ᵥ (pure b) = pure(a -ᵥ b).

Русский

Разность по вектору двух чистых фильтров равна чистому фильтру полученного вектора: (pure a) -ᵥ (pure b) = pure(a -ᵥ b).

LaTeX

$$$ (pure\ a) -ᵥ (pure\ b) = pure(a -ᵥ b)$$$

Lean4

theorem pure_vsub_pure : (pure a : Filter β) -ᵥ pure b = (pure (a -ᵥ b) : Filter α) := by simp

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