asBasis_filter

Mathlib.Order.Filter.Bases.Basic

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

English

For any filter f, f.asBasis.filter equals f; the basis representation and back preserve the filter.

Русский

Для любого фильтра f представление f.asBasis и последующая фильтрация возвращают сам фильтр f.

LaTeX

$$f.asBasis.filter = f$$

Lean4

theorem asBasis_filter (f : Filter α) : f.asBasis.filter = f :=
  Filter.ext fun _ => exists_mem_subset_iff

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

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

Разделы

Аффилиация

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