mem_iff — Mathlib

English

If l has an antitone basis s, then a set t is in l iff there exists i with s(i) ⊆ t.

Русский

Если фильтр имеет антиоснову базиса, тогда множество t принадлежит l тогда и только если существует i, такое что s(i) ⊆ t.

LaTeX

$$$$t \\in l \\iff \\exists i, s_i \\subseteq t.$$$$

Lean4

protected theorem mem_iff [Preorder ι] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s) {t : Set α} :
    t ∈ l ↔ ∃ i, s i ⊆ t :=
  hs.toHasBasis.mem_iff.trans <| by simp only [true_and]

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