image_of_prod — Mathlib

English

If y tends to g and hr holds frequently on f × g, then p x (y x) holds frequently along f.

Русский

Если y сходится к g и hr выполняется часто на f×g, то p x (y x) выполняется часто на f.

LaTeX

$$$$\text{Tendsto } y\ f\ g \rightarrow (\text{hr} \text{ frequently on } f \times g) \Rightarrow \forall^{\infty} x \in f, \; r\ x\ (y\ x).$$$$

Lean4

theorem image_of_prod {y : α → β} {r : α → β → Prop} (hy : Tendsto y f g) (hr : ∀ᶠ p in f ×ˢ g, r p.1 p.2) :
    ∀ᶠ x in f, r x (y x) := by
  obtain ⟨p, hp, q, hq, hr⟩ := eventually_prod_iff.mp hr
  filter_upwards [hp, hy.eventually hq] with _ hp hq using hr hp hq

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