omegaLimit_preimage_subset — Mathlib

English

The ω-limit of a preimage under g is contained in the ω-limit of the original set.

Русский

ω-предел предобраза под г содержится в ω-пределе исходного множества.

LaTeX

$$$$\omega f (\varphi( t, g x )) (g^{-1} s) \subseteq \omega f \varphi s.$$$$

Lean4

theorem omegaLimit_preimage_subset {α' : Type*} (ϕ : τ → α' → β) (s : Set α') (f : Filter τ) (g : α → α') :
    ω f (fun t x ↦ ϕ t (g x)) (g ⁻¹' s) ⊆ ω f ϕ s :=
  mapsTo_omegaLimit _ (mapsTo_preimage _ _) (fun _t _x ↦ rfl) continuous_id

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