filter_eq

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#Filter.HasBasis.filter_eq

English

For h : IsBasis p s, the filter h.filter equals the generate of sets {U | ∃ i, p i ∧ s i = U}.

Русский

Для h : IsBasis p s фильтр h.filter равен порождению множества {U | ∃ i, p i ∧ s i = U}.

LaTeX

$$$h.filter = \mathrm{generate}\{U \mid \exists i,\ p(i) \wedge s(i) = U\}$$$

Lean4

theorem filter_eq (h : l.HasBasis p s) : h.isBasis.filter = l :=
  by
  ext U
  simp [h.mem_iff, IsBasis.mem_filter_iff]

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

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

Разделы

Аффилиация

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