English
ContinuousWithinAt (uncurry <| lift₂ f hf) s (mk x, mk y) is equivalent to ContinuousWithinAt (uncurry f) (Prod.map mk mk⁻¹' s) (x, y).
Русский
ContinuousWithinAt (uncurry <| lift₂ f hf) s (mk x, mk y) ⇔ ContinuousWithinAt (uncurry f) (Prod.map mk mk⁻¹' s) (x, y).
LaTeX
$$ContinuousWithinAt (Function.uncurry <| SeparationQuotient.lift₂ f hf) s (Prod.mk x, Prod.mk y) ↔ ContinuousWithinAt (Function.uncurry f) (Prod.map mk mk ⁻¹' s) (x, y)$$
Lean4
@[simp]
theorem continuousWithinAt_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d}
{s : Set (SeparationQuotient X × SeparationQuotient Y)} {x : X} {y : Y} :
ContinuousWithinAt (uncurry <| lift₂ f hf) s (mk x, mk y) ↔
ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (x, y) :=
tendsto_lift₂_nhdsWithin
