mem_filter_iff — Mathlib

English

For a FilterBasis B, an arbitrary set U belongs to the associated filter if and only if there exists a basis element s ∈ B with s ⊆ U.

Русский

Для базиса фильтра B множество U принадлежит соответствующему фильтру тогда и только тогда, когда существует элемент базиса s ∈ B с подпунктом s ⊆ U.

LaTeX

$$$U \in B.\text{filter} \iff \exists s \in B, s \subseteq U$$$

Lean4

theorem mem_filter_iff (B : FilterBasis α) {U : Set α} : U ∈ B.filter ↔ ∃ s ∈ B, s ⊆ U :=
  Iff.rfl

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