eventually_mem_or_not_mem — Mathlib

English

For any L with HasSupport, any b is either eventually in L.support or eventually not in L.support.

Русский

Для любого L с HasSupport любой элемент b либо в конечном счёте принадлежит L.support, либо не принадлежит.

LaTeX

$$$ \forall {L} [HasSupport L], \forall b, (\forall^\!s in L.filter, b \in s) \lor (\forall^\!s in L.filter, b \notin s) $$$

Lean4

theorem eventually_mem_or_not_mem (L : SummationFilter β) [HasSupport L] (b : β) :
    (∀ᶠ s in L.filter, b ∈ s) ∨ (∀ᶠ s in L.filter, b ∉ s) :=
  by
  rw [or_iff_not_imp_left]
  intro hb
  filter_upwards [L.eventually_le_support] with a ha using notMem_subset ha hb

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