eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset

English

Union of omega-limits is subset of omega-limit of union.

Русский

Объединение ω‑лимитов subset ω‑лимита объединения.

LaTeX

$$$ \bigcup_i \omega f ϕ (p_i) \subseteq \omega f ϕ (\bigcup_i p_i). $$$

Lean4

theorem eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset [T2Space β] {c : Set β}
    (hc₁ : IsCompact c) (hc₂ : ∀ᶠ t in f, MapsTo (ϕ t) s c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : ω f ϕ s ⊆ n) :
    ∀ᶠ t in f, MapsTo (ϕ t) s n :=
  by
  rcases eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset f ϕ s hc₁ hc₂ hn₁ hn₂ with
    ⟨u, hu_mem, hu⟩
  refine mem_of_superset hu_mem fun t ht x hx ↦ ?_
  exact hu (subset_closure <| mem_image2_of_mem ht hx)

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