eventually_subset — Mathlib

English

If l has an antitone basis s, then for any t ∈ l, eventually i, s(i) ⊆ t along atTop.

Русский

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

LaTeX

$$$$\forall t \in l, \; \forall\!\text{eventually } i \in atTop,\; s(i) \subseteq t.$$$$

Lean4

theorem eventually_subset [Preorder ι] {l : Filter α} {s : ι → Set α} (hl : l.HasAntitoneBasis s) {t : Set α}
    (ht : t ∈ l) : ∀ᶠ i in atTop, s i ⊆ t :=
  let ⟨i, _, hi⟩ := hl.1.mem_iff.1 ht
  (eventually_ge_atTop i).mono fun _j hj => (hl.antitone hj).trans hi

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