mem — Mathlib

English

Let l be a filter on α with an antitone basis s. Then for every index i, the set s(i) belongs to l.

Русский

Пусть l — фильтр на α с антитонным основанием s. Тогда для каждого индекса i множество s(i) принадлежит l.

LaTeX

$$$\\mathrm{HasAntitoneBasis}(l,s)\\rightarrow \\forall i\\, s(i)\\in l$$$

Lean4

protected theorem mem [Preorder ι] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s) (i : ι) : s i ∈ l :=
  hs.toHasBasis.mem_of_mem trivial

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