eventually_mapsTo_of_isOpen_of_omegaLimit_subset

English

Under suitable conditions, eventually whenever t maps s into c, t maps s into n frequently for any neighborhood n of the ω-limit.

Русский

При подходящих условиях в конечной мере: если некоторые t отправляют s в c, то часто в f существует t, для которого s маппится в n, где n — окрестность ω‑лимита.

LaTeX

$$$ \forall n\, (IsOpen n)\Rightarrow \omega f ϕ s \subseteq n \Rightarrow \exists u \in f, closure(image2 ϕ u s) \subseteq n. $$$

Lean4

theorem eventually_mapsTo_of_isOpen_of_omegaLimit_subset [CompactSpace β] {v : Set β} (hv₁ : IsOpen v)
    (hv₂ : ω f ϕ s ⊆ v) : ∀ᶠ t in f, MapsTo (ϕ t) s v :=
  by
  rcases eventually_closure_subset_of_isOpen_of_omegaLimit_subset f ϕ s hv₁ hv₂ 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)

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