eventually_closure_subset_of_isOpen_of_omegaLimit_subset

English

Under a fixed f and ϕ, for each v ∈ f, the omega-limit equals an iterated intersection over f.sets with restrictions by v.

Русский

При фиксированных f и ϕ ω‑лимит равен итеративному пересечению по f.sets с ограничением по v.

LaTeX

$$$ \omega f ϕ s = \bigcap_{u \in f.sets} \overline{image2 ϕ (u \cap v) s}. $$$

Lean4

theorem eventually_closure_subset_of_isOpen_of_omegaLimit_subset [CompactSpace β] {v : Set β} (hv₁ : IsOpen v)
    (hv₂ : ω f ϕ s ⊆ v) : ∃ u ∈ f, closure (image2 ϕ u s) ⊆ v :=
  eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' _ _ _ isCompact_univ
    ⟨univ, univ_mem, subset_univ _⟩ hv₁ hv₂

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