nonempty_omegaLimit — Mathlib

English

If f is nontrivial, s is nonempty, and there exists a suitable compact c approachable by image2, then ω f ϕ s is nonempty.

Русский

Если фильтр не тождественный, s непусто, и существует компактная область, к которой стремится image2, то ω f ϕ s непуст.

LaTeX

$$$ [CompactSpace β] \Rightarrow \text{nonempty}(\omega f ϕ s) \text{ under suitable conditions.}$$$

Lean4

theorem nonempty_omegaLimit [CompactSpace β] [NeBot f] (hs : s.Nonempty) : (ω f ϕ s).Nonempty :=
  nonempty_omegaLimit_of_isCompact_absorbing _ _ _ isCompact_univ ⟨univ, univ_mem, subset_univ _⟩ hs

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