mem_iSup — Mathlib

English

For x a subset of α and a family of filters f_i, membership in the iSup of the family holds exactly when x belongs to every f_i.

Русский

Для множества x ⊆ α и семейства фильтров f_i верно, что x ∈ iSup f тогда лишь если x ∈ f_i для всех i.

LaTeX

$$$x \in \mathrm{iSup}\,f \;\iff\; \forall i,\ x \in f(i)$$$

Lean4

@[simp]
theorem mem_iSup {x : Set α} {f : ι → Filter α} : x ∈ iSup f ↔ ∀ i, x ∈ f i := by
  simp only [← Filter.mem_sets, iSup_sets_eq, mem_iInter]

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