instT0Space

Mathlib.Topology.Filter

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

English

The space of filters over any type α is a T0-space.

Русский

Пространство фильтров над любым типом α является T0-пространством.

LaTeX

$$‎$\text{T0Space}(\text{Filter}(\alpha)).$$$

Lean4

instance : T0Space (Filter α) :=
  ⟨fun _ _ h => (specializes_iff_le.1 h.specializes).antisymm (specializes_iff_le.1 h.symm.specializes)⟩

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

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

Разделы

Аффилиация

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