mem_filterBasis_iff

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#Filter.IsBasis.mem_filterBasis_iff

English

For a Filter.IsBasis structure h, the membership U ∈ h.filterBasis is equivalent to ∃ i with p i and s i = U.

Русский

Для структуры Filter.IsBasis h членство U ∈ h.filterBasis эквивалентно существованию i с p i и s i = U.

LaTeX

$$$U \in h.filterBasis \iff \exists i, p i \land s i = U$$$

Lean4

theorem mem_filterBasis_iff {U : Set α} : U ∈ h.filterBasis ↔ ∃ i, p i ∧ s i = U :=
  Iff.rfl

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

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

Разделы

Аффилиация

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