omegaLimit_image_eq — Mathlib

English

For any sets s, the ω-limit of φ on the image of s under g equals the ω-limit of φ ∘ g on s.

Русский

Для любых множеств множества ω-предел образа функции φ на образе s равен ω-пределу φ ∘ g на s.

LaTeX

$$$$\omega f ϕ (g''s) = \omega f (ϕ \circ g) s.$$$$

Lean4

theorem omegaLimit_image_eq {α' : Type*} (ϕ : τ → α' → β) (f : Filter τ) (g : α → α') :
    ω f ϕ (g '' s) = ω f (fun t x ↦ ϕ t (g x)) s := by simp only [omegaLimit, image2_image_right]

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