le_lift'_closure

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#Filter.le_lift'_closure

English

For any filter l on X, l is contained in its lift by closure: l ≤ l.lift' closure.

Русский

Для любого фильтра l на X выполнено: l ⊆ l.lift' closure.

LaTeX

$$$l \\\\leq l.lift' \\\\operatorname{closure}$$$

Lean4

theorem le_lift'_closure (l : Filter X) : l ≤ l.lift' closure :=
  le_lift'.2 fun _ h => mem_of_superset h subset_closure

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

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

Разделы

Аффилиация

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