pure_div_pure

Mathlib.Order.Filter.Pointwise

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

English

Again, the division of pure filters adheres to the rule pure(a)/pure(b) = pure(a/b).

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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