countableInterFilter_residual

Mathlib.Topology.GDelta.Basic

URI: https://scilib.ai/kg/mathlib#countableInterFilter_residual

English

The residual filter is closed under countable intersections.

Русский

Резидуальный фильтр замыкается на счетные пересечения.

LaTeX

$$∀I\\ Countable(I), ∀(F_i)_{i∈I} ⊆ residual(X), ∩_{i∈I} F_i ∈ residual(X)$$

Lean4

instance countableInterFilter_residual : CountableInterFilter (residual X) := by rw [residual]; infer_instance

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

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

Разделы

Аффилиация

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