closure_singleton

Mathlib.Topology.Filter

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

English

The closure of the singleton {l} is the upward set Ici l: all filters greater than or equal to l.

Русский

Замыкание множества {l} равно множеству Ici l: все фильтры, большие или равные l.

LaTeX

$$$\text{closure} \{l\} = \text{Ici}(l).$$$

Lean4

@[simp]
protected theorem closure_singleton (l : Filter α) : closure { l } = Ici l :=
  by
  ext l'
  simp [Filter.mem_closure, Filter.le_def]

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

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

Разделы

Аффилиация

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