English
Tendsto (uncurry <| lift₂ f hf) (nhds (mk x, mk y)) within s is equivalent to Tendsto (uncurry f) (nhdsWithin (x, y)) within preimage.
Русский
Tendsto (uncurry <| lift₂ f hf) (nhdsWithin (mk x, mk y) s) ⇔ Tendsto (uncurry f) (nhdsWithin (x, y)) в предобразе s.
LaTeX
$$Tendsto (uncurry <| lift₂ f hf) (nhdsWithin (mk x, mk y) s) l ↔ Tendsto (uncurry f) (nhdsWithin (x, y) (Set.preimage (Prod.map mk mk) s)) l$$
Lean4
@[simp]
theorem tendsto_lift₂_nhdsWithin {f : X → Y → α} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} {x : X} {y : Y}
{s : Set (SeparationQuotient X × SeparationQuotient Y)} {l : Filter α} :
Tendsto (uncurry <| lift₂ f hf) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l :=
by
rw [nhdsWithin, ← map_prod_map_mk_nhds, ← Filter.push_pull, comap_principal]
rfl
